A context-based approach to proving termination of evaluation
DOI10.1016/J.ENTCS.2009.07.090zbMATH Open1337.68061OpenAlexW2109833947MaRDI QIDQ2805157FDOQ2805157
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
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
normalization by evaluationcontrol operatorsreduction semanticsevaluation contextweak head normalization
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)
Cites Work
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- The revised report on the syntactic theories of sequential control and state
- 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
- Intensional interpretations of functionals of finite type I
- A syntactic theory of sequential control
- Representing Control: a Study of the CPS Transformation
- Proofs of strong normalisation for second order classical natural deduction
- A syntactic correspondence between context-sensitive calculi and abstract machines
- Title not available (Why is that?)
- Intuitionistic model constructions and normalization proofs
- Title not available (Why is that?)
- Program extraction from normalization proofs
- Program extraction from proofs of weak head normalization
- An Operational Foundation for Delimited Continuations in the CPS Hierarchy
- A proof-theoretic foundation of abortive continuations
- Title not available (Why is that?)
Cited In (3)
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)
