A semantic framework for proof evidence
From MaRDI portal
Publication:1701039
DOI10.1007/s10817-016-9380-6zbMath1425.68371OpenAlexW2463991046MaRDI QIDQ1701039
Fabien Renaud, Zakaria Chihani, Dale A. Miller
Publication date: 22 February 2018
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01390912/file/fpc-jar.pdf
intuitionistic logicclassical logicfocused proof systemsproof checkingfoundational proof certificatesproof certificates
Related Items
Proof checking and logic programming, A Survey of the Proof-Theoretic Foundations of Logic Programming, Towards substructural property-based testing, Proof search and certificates for evidential transactions, Complexity of translations from resolution to sequent calculus, A general proof certification framework for modal logic, A proof theory for model checking
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The future of logic: foundation-independence
- Linear logic
- Proof and refutation in MALL as a game
- A focused approach to combining logics
- Producing and verifying extremely large propositional refutations
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A logical characterization of forward and backward chaining in the inverse method
- Focusing and polarization in linear, intuitionistic, and classical logics
- A compact representation of proofs
- Implementing tactics and tacticals in a higher-order logic programming language
- Theorem proving modulo
- Isabelle/HOL. A proof assistant for higher-order logic
- Autarkic computations in formal proofs
- Proof certificates for equality reasoning
- Edinburgh LCF. A mechanized logic of computation
- The foundation of a generic theorem prover
- The origins of structural operational semantics
- SMT proof checking using a logical framework
- Proofs without syntax
- Uniform proofs as a foundation for logic programming
- HOL-λσ: an intentional first-order expression of higher-order logic
- An open logical framework
- Programming with Higher-Order Logic
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Principles and implementation of deductive parsing
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- The Proof Certifier Checkers
- Focused Labeled Proof Systems for Modal Logic
- ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter
- Classical and Intuitionistic Subexponential Logics Are Equally Expressive
- From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
- Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
- A new constructive logic: classic logic
- Logic Programming with Focusing Proofs in Linear Logic
- A framework for defining logics
- The relative efficiency of propositional proof systems
- The Impact of the Lambda Calculus in Logic and Computer Science
- Foundational Proof Certificates in First-Order Logic
- Introduction to generalized type systems
- Oracle-based checking of untrusted software
- Call-by-Value -calculus and LJQ
- Three models for the description of language
- A multi-focused proof system isomorphic to expansion proofs
- Proof Checking and Logic Programming
- Least and Greatest Fixed Points in Linear Logic
- Tools and Algorithms for the Construction and Analysis of Systems
- Solution to a problem of Ono and Komori
- The consistency of arithmetics
