Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation

DOI10.1016/J.APAL.2011.06.021zbMath1248.03024OpenAlexW1981693770MaRDI QIDQ651316

Peter Dybjer, Denis Kuperberg

Publication date: 12 December 2011

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2011.06.021

zbMATH Keywords

Haskelllazy evaluationfunctional programmingBöhm treesnormalization by evaluationcombinatory logicformal neighbourhoods

Mathematics Subject Classification ID

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

Related Items (1)

Normalization by Evaluation for Typed Weak lambda-Reduction

Uses Software

• Haskell

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A functional programming approach to the specification and verification of concurrent systems
• Comparing integrated and external logics of functional programs
• LCF considered as a programming language
• Some points in formal topology.
• Edinburgh LCF. A mechanized logic of computation
• Relational properties of domains
• A type theoretic interpretation of constructive domain theory
• Intuitionistic model constructions and normalization proofs
• A new type assignment for λ-terms
• The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
• Efficient self-interpretation in lambda calculus
• Operational aspects of untyped Normalisation by Evaluation
• Denotational aspects of untyped normalization by evaluation
• Computational adequacy via ‘mixed’ inductive definitions

This page was built for publication: Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation