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

DOI10.1016/J.APAL.2011.06.021zbMATH Open1248.03024OpenAlexW1981693770MaRDI QIDQ651316FDOQ651316

Authors: 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

Recommendations

• Denotational aspects of untyped normalization by evaluation
• Foundations of Software Science and Computation Structures
• Operational aspects of untyped Normalisation by Evaluation
• The simple type theory of normalisation by evaluation
• scientific article; zbMATH DE number 2090724

zbMATH Keywords

functional programmingcombinatory logicnormalization by evaluationlazy evaluationformal neighbourhoodsHaskellBöhm trees

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (2)

• Normalization by Evaluation for Typed Weak lambda-Reduction
• Denotational aspects of untyped normalization by evaluation

Uses Software

• Haskell

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

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