Proving termination of evaluation for system F with control operators

zbMATH Open1471.68055arXiv1309.1261MaRDI QIDQ4957787FDOQ4957787

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

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

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)

Cites Work

• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Typed Lambda Calculi and Applications
• 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
• The duality of computation
• Intensional interpretations of functionals of finite type I
• Title not available (Why is that?)
• Proofs of strong normalisation for second order classical natural deduction
• Polymorphic Delimited Continuations
• A new deconstructive logic: linear logic
• Strong normalization proofs by CPS-translations
• An Operational Foundation for Delimited Continuations in the CPS Hierarchy
• Classical \(F_{\omega}\), orthogonality and symmetric candidates
• A proof-theoretic foundation of abortive continuations
• Title not available (Why is that?)
• Defunctionalized interpreters for call-by-need evaluation
• A context-based approach to proving termination of evaluation
• Operational interpretations of an extension of F_ω with control operators

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)