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

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) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) 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

• 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
• 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?)
• 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)