Show simple item record

dc.contributor.authorMatache, Cen
dc.contributor.authorBorges Ferreira Gomes, Victoren
dc.contributor.authorMulligan, Dominicen
dc.date.accessioned2018-06-19T10:22:27Z
dc.date.available2018-06-19T10:22:27Z
dc.date.issued2017-01-01en
dc.identifier.isbn9783319712369en
dc.identifier.issn0302-9743
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/277225
dc.description.abstractThe propositions-as-types correspondence is ordinarily presen- ted as linking the metatheory of typed λ-calculi and the proof theory of intuitionistic logic. Griffin observed that this correspondence could be extended to classical logic through the use of control operators. This observation set off a flurry of further research, leading to the development of Parigot’s λμ-calculus. In this work, we use the λμ-calculus as the foundation for a system of proof terms for classical first-order logic. In particular, we define an extended call-by-value λμ-calculus with a type system in correspondence with full classical logic. We extend the language with polymorphic types, add a host of data types in ‘direct style’, and prove several metatheoretical properties. All of our proofs and definitions are mechanised in Isabelle/HOL, and we automatically obtain an inter- preter for a system of proof terms cum programming language—called μML—using Isabelle’s code generation mechanism. Atop our proof terms, we build a prototype LCF-style interactive theorem prover—called μTP— for classical first-order logic, capable of synthesising μML programs from completed tactic-driven proofs. We present example closed μML programs with classical tautologies for types, including some inexpressible as closed programs in the original λμ-calculus, and some example tactic-driven μTP proofs of classical tautologies.
dc.titleProgramming and proving with classical typesen
dc.typeConference Object
prism.endingPage234
prism.publicationDate2017en
prism.publicationNameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)en
prism.startingPage215
prism.volume10695 LNCSen
dc.identifier.doi10.17863/CAM.24518
dcterms.dateAccepted2017-11-19en
rioxxterms.versionofrecord10.1007/978-3-319-71237-6_11en
rioxxterms.versionAM*
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserveden
rioxxterms.licenseref.startdate2017-01-01en
dc.contributor.orcidBorges Ferreira Gomes, Victor [0000-0002-2954-4648]
dc.contributor.orcidMulligan, Dominic [0000-0003-4643-3541]
dc.identifier.eissn1611-3349
rioxxterms.typeConference Paper/Proceeding/Abstracten
pubs.funder-project-idEPSRC (EP/K008528/1)


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record