Gluing together proof environments: Canonical extensions of LF type theories featuring locks
File(s)
Published version
Author(s)
Honsell, F
Maksimović, P
Liquori, L
Scagnetto, I
Type
Conference Paper
Abstract
© F. Honsell, L. Liquori, P. Maksimovic, I. Scagnetto This work is licensed under the Creative Commons Attribution License. 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 gluing together diverse 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, CLLF/p,is the canonical version of the system LLF p, presented earlier by the authors. The second system, CLLF p?, features the possibility of invoking the oracle to obtain a witness satisfying a given constraint. We discuss encodings of Fitch-Prawitz Set theory, call-by-value λ-calculi, and systems of Light Linear Logic. Finally, we show how to use Fitch-Prawitz Set Theory to define a type system that types precisely the strongly normalizing terms.
Date Issued
2015-07-27
Date Acceptance
2015-01-01
Citation
Electronic Proceedings in Theoretical Computer Science, 2015, 185, pp.3-7
ISSN
2075-2180
Publisher
Open Publishing Association
Start Page
3
End Page
7
Journal / Book Title
Electronic Proceedings in Theoretical Computer Science
Volume
185
Copyright Statement
© F. Honsell, L. Liquori, P. Maksimovi´c, I. Scagnetto
This work is licensed under the
Creative Commons Attribution License.
This work is licensed under the
Creative Commons Attribution License.
License URL
Source
Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice
Subjects
cs.LO
D.2.4; F.3.1; F.4.1
Publication Status
Published
Start Date
2015-08-01
Finish Date
2015-08-01
Coverage Spatial
Berlin, Germany