A context-based approach to proving termination of evaluation

DOI10.1016/J.ENTCS.2009.07.090MaRDI QIDQ2805157zbMATH OpenOpenAlexFDO

Authors 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

normalization by evaluationcontrol operatorsreduction semanticsevaluation contextweak head normalization

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1722702
• Proving termination in the context-sensitive dependency pair framework
• Proof-theoretic analysis of termination proofs
• Using context-sensitive rewriting for proving innermost termination of rewriting
• scientific article; zbMATH DE number 1903370
• A methodology for proving termination of logic programs
• Proving termination of context-sensitive rewriting by transformation
• Proving termination of context-sensitive rewriting with MU-TERM
• Proving termination of programs automatically with AProVE
• Proving termination of (conditional) rewrite systems. A semantic approach

Cites work

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

Cited in

(3)

• Proving termination of evaluation for system F with control operators
• A Terminating Evaluation-Driven Variant of G3i
• Bisimulations for delimited-control operators

This page was built for publication: A context-based approach to proving termination of evaluation

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