Final Report of the COST-247 Action |
A logic and compositional proof system for Erlang: An overview
Fredrik Orava
KTH/Teleinformatik |
Electrum 204 |
S-164 40 KISTA |
SWEDEN |
Tel: +46 8 752 1490 |
Fax: +46 8 751 1793 |
E-mail: fredrik@it.kth.se |
In this talk we describe ongoing work on developing a compositional proof system for the concurrent functional programming language Erlang. Three main components of the work are: a (Plotkin-style) operational semantics for a core fragment of Erlang including recursion, parallelism, communication and process spawning; a specification logic for the Erlang fragment based on the modal mu-calculus; and a compositional proof system for establishing that Erlang programs possesses properties expressed in the specification logic. The proof system is based on an early prototype tool for the pi-calculus developed at SICS. An early implementation of the system can be demonstrated on request.
This presentation has been given during the COST-247 7th Management Committee Meeting (Madrid, Spain, February, 12-13, 1995).
COST-247 Working Group(s): 2
This Page was prepared by Mark Jorgensen.