Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation
type: Item
instance of: scholarly article
title: Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation
zbMATH Open document ID: 1248.03024
author: Peter Dybjer
author: Denis Kuperberg
published in: Annals of Pure and Applied Logic
publication date: 2011-12-12T00:00:00Z
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 68N18
zbMATH DE Number: 5987966
zbMATH Keywords: combinatory logic
zbMATH Keywords: normalization by evaluation
zbMATH Keywords: formal neighbourhoods
zbMATH Keywords: lazy evaluation
zbMATH Keywords: Böhm trees
zbMATH Keywords: functional programming
zbMATH Keywords: Haskell
describes a project that uses: Haskell
MaRDI profile type: Publication
full work available at URL: j.apal.2011.06.021
OpenAlex ID: W1981693770
cites work: Operational aspects of untyped Normalisation by Evaluation
cites work: Q3221960
cites work: Q4281467
cites work: Intuitionistic model constructions and normalization proofs
cites work: A new type assignment for λ-terms
cites work: Q4440321
cites work: A functional programming approach to the specification and verification of concurrent systems
cites work: Q3685173
cites work: Comparing integrated and external logics of functional programs
cites work: Q4494371
cites work: Denotational aspects of untyped normalization by evaluation
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: A type theoretic interpretation of constructive domain theory
cites work: Q4099614
cites work: Q4099613
cites work: Efficient self-interpretation in lambda calculus
cites work: Computational adequacy via ‘mixed’ inductive definitions
cites work: Relational properties of domains
cites work: LCF considered as a programming language
cites work: Q3481701
cites work: Some points in formal topology.
cites work: Q3664454
cites work: Q3959414
cites work: The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
DOI: 10.1016/J.APAL.2011.06.021
description: scientific article; zbMATH DE number 5987966