Towards normalization by evaluation for the -calculus of constructions

DOI10.1007/978-3-642-12251-4_17MaRDI QIDQ3558341zbMATH OpenOpenAlexFDO

Authors Andreas Abel

Publication date 4 May 2010

Published in Functional and Logic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-12251-4_17

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• The simple type theory of normalisation by evaluation
• On the proof theory of Coquand's calculus of constructions
• Normalization by Evaluation for Martin-Löf Type Theory with One Universe
• Foundations of Software Science and Computation Structures
• scientific article; zbMATH DE number 1330132

Cited in

(1)

• Pure type systems with explicit substitutions

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Towards normalization by evaluation for the \(\beta \eta \)-calculus of constructions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3558341)