Towards normalization by evaluation for the -calculus of constructions

DOI10.1007/978-3-642-12251-4_17zbMATH Open1284.68120OpenAlexW1599601364MaRDI QIDQ3558341FDOQ3558341

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

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Cited In (1)

• Pure type systems with explicit substitutions

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)