A domain model characterising strong normalisation

DOI10.1016/J.APAL.2008.06.005MaRDI QIDQ958484zbMATH OpenOpenAlexFDO

Authors Ulrich Berger

Publication date 5 December 2008

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.2008.06.005

zbMATH Keywords

domain theoryterm rewritingnormalisation\(\lambda \)-calculus

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• A proof of strong normalisation using domain theory
• Strong normalization in type systems: A model theoretical approach
• Foundations of Software Science and Computation Structures
• Abstracting models of strong normalization for classical calculi
• A domain-theoretic model of nominally-typed object-oriented programming
• Domain-specific semantics and data refinement of object models
• A Practical Alternative to Domain and Type Enforcement Integrity Formal Models
• Domain theoretic models of polymorphism

Cites work

• scientific article; zbMATH DE number 1696608 (Why is no real title available?)
• scientific article; zbMATH DE number 3735770 (Why is no real title available?)
• scientific article; zbMATH DE number 3440411 (Why is no real title available?)
• scientific article; zbMATH DE number 1405632 (Why is no real title available?)
• scientific article; zbMATH DE number 3231083 (Why is no real title available?)
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A filter lambda model and the completeness of type assignment
• Adding algebraic rewriting to the untyped lambda calculus
• An elementary proof of strong normalization for intersection types
• Complete restrictions of the intersection type discipline
• Continuous Lattices and Domains
• Counterexamples to termination for the direct sum of term rewriting systems
• Definitions by rewriting in the Calculus of Constructions
• LCF considered as a programming language
• Logical Approaches to Computational Barriers
• New Computational Paradigms
• Normalization without reducibility
• Notions of computation and monads
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Strong normalisation for applied lambda calculi
• Termination for direct sums of left-linear complete term rewriting systems

Cited in

(6)

• Strong normalisation for applied lambda calculi
• A proof of strong normalisation using domain theory
• A behavioural model for Klop's calculus
• Size-based termination of higher-order rewriting
• New Computational Paradigms
• Continuous semantics for strong normalisation

This page was built for publication: A domain model characterising strong normalisation

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