A functional interpretation with state

DOI10.1145/3209108.3209134MaRDI QIDQ5145361zbMATH OpenOpenAlexFDO

Authors

Publication date 20 January 2021

Published in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3209108.3209134

zbMATH Keywords

program extractionfunctional interpretationstate monad

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Relative consistency and interpretations (03F25) Functionals in proof theory (03F10)

Recommendations

• Computer Science Logic
• Quasi-linear Dialectica Extraction
• A complexity analysis of functional interpretations
• Dialectica interpretation with marked counterexamples
• Analysis of methods for extraction of programs from non-constructive proofs.

Cited in

(7)

• scientific article; zbMATH DE number 7269245 (Why is no real title available?)
• Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
• A complexity analysis of functional interpretations
• A finitization of Littlewood's Tauberian theorem and an application in Tauberian remainder theory
• A Gentzen-style monadic translation of Gödel's system T
• Stateful Realizers for Nonstandard Analysis
• A functional functional interpretation

This page was built for publication: A functional interpretation with state

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