Controlling Program Extraction in Light Logics

DOI10.1007/978-3-642-21691-6_12MaRDI QIDQ3007661zbMATH OpenOpenAlexFDO

Authors Marc Lasson

Publication date 17 June 2011

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-21691-6_12

Mathematics Subject Classification ID

Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Recommendations

• scientific article; zbMATH DE number 2003148
• scientific article; zbMATH DE number 1189111
• Extracting program logics from abstract interpretations defined by logical relations
• Program Extraction in Constructive Analysis
• Completeness, minimal logic and programs extraction
• An operational approach to program extraction in the calculus of constructions
• Light affine logic as a programming language: a first contribution
• Logic + control: on program construction and verification
• Practical program extraction from classical proofs
• A CTL-based logic for program abstractions

Cites work

• scientific article; zbMATH DE number 1722649 (Why is no real title available?)
• scientific article; zbMATH DE number 2185725 (Why is no real title available?)
• scientific article; zbMATH DE number 4147469 (Why is no real title available?)
• scientific article; zbMATH DE number 482822 (Why is no real title available?)
• Intuitionistic light affine logic
• Light linear logic
• Realizability and parametricity in pure type systems
• The Girard-Reynolds isomorphism (second edition)
• Type inference for light affine logic via constraints on words

This page was built for publication: Controlling Program Extraction in Light Logics

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