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 Constructions, 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 annotations 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.
Work supported by MIUR PRIN project 20088HXMYN, “SisteR”.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Armstrong, J.: Erlang - a survey of the language and its industrial applications. In: Proc. INAP 1996 (1996)
Honsell, F., Miculan, M.: A Natural Deduction Approach to Dynamic Logics. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158, pp. 165–182. Springer, Heidelberg (1996)
Honsell, F., Miculan, M., Scagnetto, I.: π-calculus in (co)inductive type theory. Theoretical Computer Science 253(2), 239–285 (2001)
Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Proc. POPL, pp. 42–54. ACM (2006)
Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)
Letouzey, P.: Extraction in COQ: An Overview. In: Beckmann, A., Dimitracopoulos, C., Löwe, B. (eds.) CiE 2008. LNCS, vol. 5028, pp. 359–369. Springer, Heidelberg (2008)
Licata, D.R., Harper, R.: A monadic formalization of ML5. In: Crary, K., Miculan, M. (eds.) Proc. LFMTP. EPTCS, vol. 34, pp. 69–83 (2010)
Murphy VII, T., Crary, K., Harper, R.: Type-Safe Distributed Programming with ML5. In: Barthe, G., Fournet, C. (eds.) TGC 2007. LNCS, vol. 4912, pp. 108–123. Springer, Heidelberg (2008)
Paulin-Mohring, C., Werner, B.: Synthesis of ML programs in the system COQ. Journal of Symbolic Computation 15, 607–640 (1993)
Plotkin, G., Power, J.: Notions of Computation Determine Monads. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 342–356. Springer, Heidelberg (2002)
Virding, R., Wikström, C., Williams, M.: Concurrent programming in ERLANG, 2nd edn. Prentice Hall International (UK) Ltd. (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Miculan, M., Paviotti, M. (2012). Synthesis of Distributed Mobile Programs Using Monadic Types in Coq. In: Beringer, L., Felty, A. (eds) Interactive Theorem Proving. ITP 2012. Lecture Notes in Computer Science, vol 7406. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32347-8_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-32347-8_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32346-1
Online ISBN: 978-3-642-32347-8
eBook Packages: Computer ScienceComputer Science (R0)