Proofs as efficient programs

DOI10.1007/978-88-470-0784-0_8MaRDI QIDQ3654818zbMATH OpenOpenAlexFDO

Authors Ugo Dal Lago, Simone Martini

Publication date 11 January 2010

Published in Deduction, Computation, Experiment (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-88-470-0784-0_8

zbMATH Keywords

complexity classCurry-Howard correspondenceimplicit computational complexitysurvey paper

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Complexity of proofs (03F20) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15)

Recommendations

• scientific article; zbMATH DE number 1469885
• Implicit computation complexity in higher-order programming languages
• scientific article; zbMATH DE number 963644
• Proofs and programs
• Lectures on the Curry-Howard isomorphism

Cited in

(6)

• Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs
• Connecting logical representations and efficient computations
• A Formal Proof of Square Root and Division Elimination in Embedded Programs
• PROVING PRODUCTIVITY IN INFINITE DATA STRUCTURES
• New Computational Paradigms
• Formal proof of a program: find

This page was built for publication: Proofs as efficient programs

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