Skip to main content
Kent Academic Repository

Synthesis of distributed mobile programs using monadic types in Coq

Miculan, Marino, Paviotti, Marco (2012) Synthesis of distributed mobile programs using monadic types in Coq. In: Proceedings of 3rd International Conference on Interactive Theorem Proving. . pp. 183-200. Springer (doi:10.1007/978-3-642-32347-8_13) (Access to this publication is currently restricted. You may be able to access a copy if URLs are provided) (KAR id:65009)

PDF Author's Accepted Manuscript
Language: English

Restricted to Repository staff only
[thumbnail of itp12.pdf]
Official URL:
http://dx.doi.org/10.1007/978-3-642-32347-8_13

Abstract

We present a methodology for the automatic synthesis of certified, distributed, mobile programs with side effects in Erlang, using the Coq proof assistant.

First, we define monadic types in the Calculus of Inductive Construc- tions, using a lax monad covering the distributed computational aspects. These types can be used for the specifications of programs in Coq. From the (constructive) proofs of these specifications we can extract Haskell code, which is decorated with symbols representing distributed nodes and specific operations for distributed computations. These syntactic anno- tations are exploited by a back-end compiler to produce actual mobile code for a suitable runtime environment (Erlang, in our case).

Then, we introduce an object type theory for distributed computations, which can be used as a front-end programming language. These types and terms are translate to CIC extended with monadic types; this allows us to prove the soundess of the object type theory, and to obtain an implementation of the language via Coq’s extraction features.

This methodology can be ported to other computational aspects, by suitably adapting the monadic type theory and the back-end compiler.

Item Type: Conference or workshop item (Paper)
DOI/Identification number: 10.1007/978-3-642-32347-8_13
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Marco Paviotti
Date Deposited: 05 Dec 2017 14:58 UTC
Last Modified: 21 Dec 2022 19:45 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/65009 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.