Getting results from programs extracted from classical proofs

DOI10.1016/j.tcs.2004.03.006zbMath1105.68022OpenAlexW1989920000MaRDI QIDQ1882897

Christophe Raffalli

Publication date: 1 October 2004

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2004.03.006

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

Unnamed Item ⋮ Unnamed Item ⋮ Programs from proofs using classical dependent choice

Uses Software

• PhoX

Cites Work

• Unnamed Item
• Unnamed Item
• A general storage theorem for integers in call-by-name \(\lambda\)- calculus
• Mixed logic and storage operators
• The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction
• Dependent choice, `quote' and the clock
• Pruning simply typed  -terms
• A semantics of evidence for classical arithmetic
• Refined program extraction from classical proofs

This page was built for publication: Getting results from programs extracted from classical proofs