Operational aspects of untyped Normalisation by Evaluation
From MaRDI portal
Publication:4818938
DOI10.1017/S096012950400427XzbMath1090.68018OpenAlexW2159526276MaRDI QIDQ4818938
Felix Joachimski, Klaus Aehlig
Publication date: 24 September 2004
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s096012950400427x
Related Items
Syntactic analysis of \(\eta\)-expansions in pure type systems. ⋮ A compiled implementation of normalisation by evaluation ⋮ Denotational aspects of untyped normalization by evaluation ⋮ Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters ⋮ On Normalization by Evaluation for Object Calculi ⋮ Internal models of system F for decompilation ⋮ Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation ⋮ A Compiled Implementation of Normalization by Evaluation ⋮ A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance ⋮ Normalization by Evaluation for Typed Weak lambda-Reduction ⋮ Normalization by Evaluation for Martin-Löf Type Theory with One Universe
Uses Software
This page was built for publication: Operational aspects of untyped Normalisation by Evaluation
