Paper Info
Title
Type-and-scope safe programs and their proofs.
Abstract
We abstract the common type-and-scope safe structure from computations on λ-terms that deliver, e.g., renaming, substitution, evaluation, CPS-transformation, and printing with a name supply. By exposing this structure, we can prove generic simulation and fusion lemmas relating operations built this way. This work has been fully formalised in Agda.
Year
DOI
Venue
2017
10.1145/3018610.3018613
CPP
Keywords
Field
DocType
Lambda-calculus, Mechanized Meta-Theory, Normalisation by Evaluation, Semantics, Generic Programming, Agda
Lambda calculus,Programming language,Normalisation by evaluation,Computer science,Algorithm,Mathematical proof,Agda,Generic programming,Lemma (mathematics),Semantics,Formal verification
Conference
Citations 
PageRank 
References 
5
0.45
19
Authors
4
Name
Order
Citations
PageRank
Guillaume Allais150.45
James Chapman2445.27
Conor McBride375247.89
james mckinna446443.02