Operational aspects of untyped Normalisation by Evaluation

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items (11)

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

• Haskell

This page was built for publication: Operational aspects of untyped Normalisation by Evaluation