Compiling with classical connectives

MaRDI QIDQ5119393zbMATH OpenFDO

Authors Paul Downen, Zena M. Ariola

Publication date 4 September 2020

Full work available at URL https://arxiv.org/abs/1907.13227, https://lmcs.episciences.org/6740

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• Beyond polarity: towards a multi-discipline intermediate language with sharing
• On the unity of duality
• Classical call-by-need and duality
• Classical by-need
• Call-by-value is dual to call-by-name

Cites work

• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 4047683 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 3485174 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• A systematic approach to delimited control with multiple prompts
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Call-by-push-value: Decomposing call-by-value and call-by-name
• Call-by-value is dual to call-by-name
• Classical call-by-need and duality
• Compositional CompCert
• Compositional semantics for composable continuations: from abortive to delimited control
• Deep specifications and certified abstraction layers
• Delimited control and computational effects
• Focalisation and Classical Realisability
• Formulae-as-types for an involutive negation
• Jumbo λ-Calculus
• Logic Programming with Focusing Proofs in Linear Logic
• Models of a non-associative composition
• On the expressive power of programming languages
• On the unity of duality
• Practical foundations for programming languages
• Sequent calculus as a compiler intermediate language
• The Duality of Construction
• The call-by-need lambda calculus
• The duality of computation
• Types and programing languages
• Untersuchungen über das logische Schliessen. I
• Verified Compilation for Shared-Memory C
• Verifying an Open Compiler Using Multi-language Semantics

Describes a project that uses

Uses Software

• CompCert

This page was built for publication: Compiling with classical connectives

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