Proving termination of evaluation for system F with control operators

MaRDI QIDQ4957787zbMATH OpenFDO

Authors Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Marek Materzok

Publication date 9 September 2021

Full work available at URL https://arxiv.org/abs/1309.1261, http://eptcs.web.cse.unsw.edu.au/paper.cgi?COS2013.2

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Recommendations

• A context-based approach to proving termination of evaluation
• Operational interpretations of an extension of F_ω with control operators
• scientific article; zbMATH DE number 1070627
• Typed Lambda Calculi and Applications
• Complete call-by-value calculi of control operators. II: Strong termination

Cites work

• scientific article; zbMATH DE number 1670484 (Why is no real title available?)
• scientific article; zbMATH DE number 5851813 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 1070627 (Why is no real title available?)
• A context-based approach to proving termination of evaluation
• A new deconstructive logic: linear logic
• A proof-theoretic foundation of abortive continuations
• A syntactic approach to type soundness
• An Operational Foundation for Delimited Continuations in the CPS Hierarchy
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Classical \(F_{\omega}\), orthogonality and symmetric candidates
• Defunctionalized interpreters for call-by-need evaluation
• Intensional interpretations of functionals of finite type I
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Operational interpretations of an extension of F_ω with control operators
• Polymorphic Delimited Continuations
• Proofs of strong normalisation for second order classical natural deduction
• Strong normalization proofs by CPS-translations
• The duality of computation
• Typed Lambda Calculi and Applications

Cited in

(1)

• Bisimulations for delimited-control operators

This page was built for publication: Proving termination of evaluation for system F with control operators

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