Abstract
We present a generic framework that facilitates object level reasoning with logics that are encoded within the Higher Order Logic theorem proving environment of HOL Light. This involves proving statements in any logic using intuitive forward and backward chaining in a sequent calculus style. It is made possible by automated machinery that take care of the necessary structural reasoning and term matching automatically. Our framework can also handle type theoretic correspondences of proofs, effectively allowing the type checking and construction of computational processes via proof. We demonstrate our implementation using a simple propositional logic and its Curry-Howard correspondence to the lambda-calculus, and argue its use with linear logic and its various correspondences to session types.
Original language | English |
---|---|
Title of host publication | Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2020) |
Editors | Claudio Sacerdoti Coen, Alwen Tiu |
Place of Publication | Paris, France |
Publisher | Open Publishing Association |
Pages | 18-34 |
Number of pages | 17 |
DOIs | |
Publication status | Published - 12 Jan 2021 |
Event | Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice - Virtual Duration: 29 Jun 2020 → 30 Jun 2020 https://lfmtp.org/workshops/2020/home.shtml |
Publication series
Name | Electronic Proceedings in Theoretical Computer Science |
---|---|
Publisher | Open Publishing Association |
Volume | 332 |
ISSN (Electronic) | 2075-2180 |
Workshop
Workshop | Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice |
---|---|
Abbreviated title | LFMTP 2020 |
Period | 29/06/20 → 30/06/20 |
Internet address |