A Monadic Formalization of ML5 - Computer Science > Programming LanguagesReportar como inadecuado

A Monadic Formalization of ML5 - Computer Science > Programming Languages - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

Abstract: ML5 is a programming language for spatially distributed computing, based on aCurry-Howard correspondence with the modal logic S5. Despite being designed bya correspondence with S5 modal logic, the ML5 programming language differs fromthe logic in several ways. In this paper, we explain these discrepanciesbetween ML5 and S5 by translating ML5 into a slightly different logic:intuitionistic S5 extended with a lax modality that encapsulates effectfulcomputations in a monad. This translation both explains the existing ML5 designand suggests some simplifications and generalizations. We have formalized ourtranslation within the Agda proof assistant. Rather than formalizing lax S5 asa proof theory, we \emph{embed} it as a universe within the the dependentlytyped host language, with the universe elimination given by implementing themodal logic-s Kripke semantics. This representation technique saves us the workof defining a proof theory for the logic and proving it correct, andadditionally allows us to inherit the equational theory of the meta-language,which can be exploited in proving that the semantics validates the operationalsemantics of ML5.

Autor: Daniel R. Licata Carnegie Mellon University, Robert Harper Carnegie Mellon University

Fuente: https://arxiv.org/

Documentos relacionados