Object-level reasoning with logics encoded in HOL Light

DOI10.4204/EPTCS.332.2MaRDI QIDQ6940471zbMATH OpenFDO

Authors Petros Papapanagiotou, Jacques D. Fleuriot

Publication date 19 August 2025

Copyright license Creative Commons license

Full work available at URL https://doi.org/10.4204/EPTCS.332.2

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• A pragmatic, scalable approach to correct-by-construction process composition using classical linear logic inference
• An Isabelle-like procedural mode for HOL Light
• Complexity of unification problems with associative-commutative operators
• Cut reduction in linear logic as asynchronous session-typed communication
• Diagrammatic representation and inference. 7th international conference, Diagrams 2012, Canterbury, UK, July 2--6, 2012. Proceedings
• Edinburgh LCF. A mechanized logic of computation
• Forum: A multiple-conclusion specification logic
• Generic methods for formalising sequent calculi applied to provability logic
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 786485 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle. A generic theorem prover
• On the \(\pi\)-calculus and linear logic
• Programming with higher-order logic.
• Proof-carrying code in a session-typed process calculus
• Proofs as processes
• Propositions as sessions
• Session types as intuitionistic linear propositions

This page was built for publication: Object-level reasoning with logics encoded in HOL Light

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