A Context-based Approach to Proving Termination of Evaluation

DOI10.1016/j.entcs.2009.07.090zbMath1337.68061OpenAlexW2109833947MaRDI QIDQ2805157

Małgorzata Biernacka, Dariusz Biernacki

Publication date: 10 May 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2009.07.090

zbMATH Keywords

reduction semanticsnormalization by evaluationcontrol operatorsevaluation contextweak head normalization

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Unnamed Item ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Program extraction from normalization proofs
• A syntactic correspondence between context-sensitive calculi and abstract machines
• A syntactic theory of sequential control
• The revised report on the syntactic theories of sequential control and state
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• A syntactic approach to type soundness
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• A proof-theoretic foundation of abortive continuations
• Intuitionistic model constructions and normalization proofs
• Representing Control: a Study of the CPS Transformation
• Proofs of strong normalisation for second order classical natural deduction
• An Operational Foundation for Delimited Continuations in the CPS Hierarchy
• Intensional interpretations of functionals of finite type I

This page was built for publication: A Context-based Approach to Proving Termination of Evaluation