Interacting Safely with an Unsafe Environment

Gilles Dowek
(Inria and ENS Paris-Saclay)

We give a presentation of Pure type systems where contexts need not be well-formed and show that this presentation is equivalent to the usual one. The main motivation for this presentation is that, when we extend Pure type systems with computation rules, like in the logical framework Dedukti, we want to declare the constants before the computation rules that are needed to check the well-typedness of their type.

In Elaine Pimentel and Enrico Tassi: Proceedings Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2021), Pittsburgh, USA, 16th July 2021, Electronic Proceedings in Theoretical Computer Science 337, pp. 30–38.
Published: 16th July 2021.

ArXived at: http://dx.doi.org/10.4204/EPTCS.337.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org