Denotational aspects of untyped normalization by evaluation

DOI10.1051/ITA:2005026zbMath1096.03010OpenAlexW2149531431MaRDI QIDQ5313717

Henning Korsholm Rohde, Andrezej Filinski

Publication date: 1 September 2005

Published in: RAIRO - Theoretical Informatics and Applications (Search for Journal in Brave)

Full work available at URL: http://www.numdam.org/item?id=ITA_2005__39_3_423_0

zbMATH Keywords

denotational semanticsfunctional programmingBöhm treesuntyped \(\lambda\)-calculuscomputational adequacynormalization-by-evaluation construction

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Continuous lattices and posets, applications (06B35) Combinatory logic and lambda calculus (03B40)

Related Items (4)

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 ⋮ Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation

Uses Software

• Unnamed Item
• Freshml

Cites Work

• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• LCF considered as a programming language
• Relational properties of domains
• Intuitionistic model constructions and normalization proofs
• A compiled implementation of strong reduction
• Operational aspects of untyped Normalisation by Evaluation
• FreshML
• Foundations of Software Science and Computation Structures
• Denotational aspects of untyped normalization by evaluation

This page was built for publication: Denotational aspects of untyped normalization by evaluation