Object-Level Reasoning with Logics Encoded in HOL Light

Petros Papapanagiotou, Jacques Fleuriot

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish
Title of host publicationProceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2020)
EditorsClaudio Sacerdoti Coen, Alwen Tiu
Place of PublicationParis, France
PublisherOpen Publishing Association
Pages18-34
Number of pages17
DOIs
Publication statusPublished - 12 Jan 2021
EventFifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice - Virtual
Duration: 29 Jun 202030 Jun 2020
https://lfmtp.org/workshops/2020/home.shtml

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
Volume332
ISSN (Electronic)2075-2180

Workshop

WorkshopFifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
Abbreviated titleLFMTP 2020
Period29/06/2030/06/20
Internet address

Fingerprint

Dive into the research topics of 'Object-Level Reasoning with Logics Encoded in HOL Light'. Together they form a unique fingerprint.

Cite this