Skip to Main content Skip to Navigation
New interface
Journal articles

Plugging-in Proof Development Environments using Locks in LF

Furio Honsell 1 Luigi Liquori 2 Petar Maksimovic 3 Ivan Scagnetto 1 
2 KAIROS - Logical Time for Formal Embedded System Design
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : We present two extensions of the LF Constructive Type Theory featuring monadic locks. A lock is a monadic type construct that captures the effect of an external call to an oracle. Such calls are the basic tool for plugging-in, i.e. gluing together, different Type Theories and proof development environments. The oracle can be invoked either to check that a constraint holds or to provide a suitable witness. The systems are presented in the canonical style developed by the "CMU School". The first system, CLLFP , is the canonical version of the system LLFP, presented earlier by the authors. The second system, CLLF P? , features the possibility of invoking the oracle to obtain also a witness satisfying a given constraint. We discuss encodings of Fitch-Prawitz Set theory, call-by-value λ-calculi, systems of Light Linear Logic, and partial functions.
Keywords : MSCS
Complete list of metadata

Cited literature [39 references]  Display  Hide  Download
Contributor : Luigi Liquori Connect in order to contact the contributor
Submitted on : Thursday, February 11, 2016 - 11:07:02 AM
Last modification on : Thursday, August 4, 2022 - 4:59:30 PM
Long-term archiving on: : Thursday, May 12, 2016 - 5:31:41 PM


Files produced by the author(s)


  • HAL Id : hal-01272647, version 1



Furio Honsell, Luigi Liquori, Petar Maksimovic, Ivan Scagnetto. Plugging-in Proof Development Environments using Locks in LF. Mathematical Structures in Computer Science, 2018, 28 (9), pp.1578--1605. ⟨hal-01272647⟩



Record views


Files downloads