Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk)

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

IsaFoL (Isabelle Formalization of Logic) is an undertaking that aims at developing formal theories about logics, proof systems, and automatic provers, using Isabelle/HOL. At the heart of the project is the conviction that proof assistants have become mature enough to actually help researchers in automated reasoning when they develop new calculi and tools. In this paper, I describe and reflect on three verification subprojects to which I contributed: A first-order resolution prover, an imperative SAT solver, and generalized term orders for-free higher-order logic.

LanguageEnglish
Title of host publicationCPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019
EditorsAssia Mahboubi
PublisherAssociation for Computing Machinery, Inc
Pages1-13
Number of pages13
ISBN (Electronic)9781450362221
DOIs
Publication statusPublished - 14 Jan 2019
Event8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019 - Cascais, Portugal
Duration: 14 Jan 201915 Jan 2019

Conference

Conference8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019
CountryPortugal
CityCascais
Period14/01/1915/01/19

Keywords

  • proof assistants
  • proof systems
  • theorem provers

Cite this

Blanchette, J. C. (2019). Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). In A. Mahboubi (Ed.), CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019 (pp. 1-13). Association for Computing Machinery, Inc. https://doi.org/10.1145/3293880.3294087
Blanchette, Jasmin Christian. / Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019. editor / Assia Mahboubi. Association for Computing Machinery, Inc, 2019. pp. 1-13
@inproceedings{c07c32c3ba6a4e1ba7403b9ee65f5d6c,
title = "Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk)",
abstract = "IsaFoL (Isabelle Formalization of Logic) is an undertaking that aims at developing formal theories about logics, proof systems, and automatic provers, using Isabelle/HOL. At the heart of the project is the conviction that proof assistants have become mature enough to actually help researchers in automated reasoning when they develop new calculi and tools. In this paper, I describe and reflect on three verification subprojects to which I contributed: A first-order resolution prover, an imperative SAT solver, and generalized term orders for-free higher-order logic.",
keywords = "proof assistants, proof systems, theorem provers",
author = "Blanchette, {Jasmin Christian}",
year = "2019",
month = "1",
day = "14",
doi = "10.1145/3293880.3294087",
language = "English",
pages = "1--13",
editor = "Assia Mahboubi",
booktitle = "CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019",
publisher = "Association for Computing Machinery, Inc",

}

Blanchette, JC 2019, Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). in A Mahboubi (ed.), CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019. Association for Computing Machinery, Inc, pp. 1-13, 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, 14/01/19. https://doi.org/10.1145/3293880.3294087

Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). / Blanchette, Jasmin Christian.

CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019. ed. / Assia Mahboubi. Association for Computing Machinery, Inc, 2019. p. 1-13.

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk)

AU - Blanchette, Jasmin Christian

PY - 2019/1/14

Y1 - 2019/1/14

N2 - IsaFoL (Isabelle Formalization of Logic) is an undertaking that aims at developing formal theories about logics, proof systems, and automatic provers, using Isabelle/HOL. At the heart of the project is the conviction that proof assistants have become mature enough to actually help researchers in automated reasoning when they develop new calculi and tools. In this paper, I describe and reflect on three verification subprojects to which I contributed: A first-order resolution prover, an imperative SAT solver, and generalized term orders for-free higher-order logic.

AB - IsaFoL (Isabelle Formalization of Logic) is an undertaking that aims at developing formal theories about logics, proof systems, and automatic provers, using Isabelle/HOL. At the heart of the project is the conviction that proof assistants have become mature enough to actually help researchers in automated reasoning when they develop new calculi and tools. In this paper, I describe and reflect on three verification subprojects to which I contributed: A first-order resolution prover, an imperative SAT solver, and generalized term orders for-free higher-order logic.

KW - proof assistants

KW - proof systems

KW - theorem provers

UR - http://www.scopus.com/inward/record.url?scp=85061191555&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85061191555&partnerID=8YFLogxK

U2 - 10.1145/3293880.3294087

DO - 10.1145/3293880.3294087

M3 - Conference contribution

SP - 1

EP - 13

BT - CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019

A2 - Mahboubi, Assia

PB - Association for Computing Machinery, Inc

ER -

Blanchette JC. Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). In Mahboubi A, editor, CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019. Association for Computing Machinery, Inc. 2019. p. 1-13 https://doi.org/10.1145/3293880.3294087