Title
Interacting Safely with an Unsafe Environment.
Abstract
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.
Year
DOI
Venue
2021
10.4204/EPTCS.337.3
International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP)
DocType
ISSN
Citations 
Conference
EPTCS 337, 2021, pp. 30-38
0
PageRank 
References 
Authors
0.34
0
1
Name
Order
Citations
PageRank
Gilles Dowek101.35