Typeful normalization by evaluation

DOI10.4230/LIPICS.TYPES.2014.72MaRDI QIDQ5277972zbMATH OpenOpenAlexFDO

Authors Olivier Danvy, Chantal Keller, Matthias Puech

Publication date 12 July 2017

Full work available at URL https://prosecco.gforge.inria.fr/personal/ckeller/Documents-recherche/Publications/types14.pdf

zbMATH Keywords

continuation-passing stylegeneralized algebraic data typesnormalization by evaluationpartial evaluation

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Abstract data types; algebraic specification (68Q65)

Recommendations

• The simple type theory of normalisation by evaluation
• Operational aspects of untyped Normalisation by Evaluation
• scientific article; zbMATH DE number 2090724
• Normalization by evaluation with typed abstract syntax
• A Compiled Implementation of Normalization by Evaluation

Cited in

(12)

• The simple type theory of normalisation by evaluation
• A compiled implementation of normalisation by evaluation
• Normalization by evaluation with typed abstract syntax
• Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums
• On Normalization by Evaluation for Object Calculi
• A Compiled Implementation of Normalization by Evaluation
• Typed Applicative Structures and Normalization by Evaluation for System F ω
• scientific article; zbMATH DE number 2090724 (Why is no real title available?)
• Operational aspects of untyped Normalisation by Evaluation
• Functional and Logic Programming
• Normalisation by evaluation for dependent types
• Normalisation by evaluation for type theory, in type theory

Describes a project that uses

Uses Software

• OCaml

This page was built for publication: Typeful normalization by evaluation

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