Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics

Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics

Church's Higher Order Logic is a basis for influential proof assistants -- HOL and PVS. Church's logic has a simple set-theoretic semantics, making it trustworthy and extensible. We factor HOL into a constructive core plus axioms of excluded middle and choice. We similarly factor standard...

पूर्ण विवरण

ग्रंथसूची विवरण
मुख्य लेखकों:	Robert Constable, Wojciech Moczydlowski
स्वरूप:	लेख
भाषा:	English
प्रकाशित:	Logical Methods in Computer Science e.V. 2008-09-01
श्रृंखला:	Logical Methods in Computer Science
विषय:	computer science - logic in computer science f.4.1
ऑनलाइन पहुंच:	https://lmcs.episciences.org/1140/pdf

समान संसाधन

Normalization of IZF with Replacement
द्वारा: Wojciech Moczydlowski
प्रकाशित: (2008-04-01)

A Normalizing Intuitionistic Set Theory with Inaccessible Sets
द्वारा: Wojciech Moczydlowski
प्रकाशित: (2007-08-01)

Classical BI: Its Semantics and Proof Theory
द्वारा: James Brotherston, और अन्य
प्रकाशित: (2010-07-01)

Intuitionistic Layered Graph Logic: Semantics and Proof Theory
द्वारा: Simon Docherty, और अन्य
प्रकाशित: (2018-10-01)

A Finite-Model-Theoretic View on Propositional Proof Complexity
द्वारा: Erich Grädel, और अन्य
प्रकाशित: (2022-06-01)

The descriptive set-theoretic complexity of the set of points of continuity of a multi-valued function
द्वारा: Vassilios Gregoriades
प्रकाशित: (2011-11-01)

From Proof Nets to the Free *-Autonomous Category
द्वारा: Francois Lamarche, और अन्य
प्रकाशित: (2006-10-01)

A proof system for graph (non)-isomorphism verification
द्वारा: Milan Banković, और अन्य
प्रकाशित: (2023-02-01)

Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
द्वारा: Assia Mahboubi, और अन्य
प्रकाशित: (2012-02-01)

A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems
द्वारा: Stéphane Jean Eric Lengrand, और अन्य
प्रकाशित: (2011-03-01)

A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
द्वारा: Andreas Abel, और अन्य
प्रकाशित: (2011-05-01)

On completeness of reducibility candidates as a semantics of strong normalization
द्वारा: Denis Cousineau
प्रकाशित: (2012-02-01)

On the strength of proof-irrelevant type theories
द्वारा: Benjamin Werner
प्रकाशित: (2008-09-01)

Kripke Semantics for Martin-L\"of's Extensional Type Theory
द्वारा: Steve Awodey, और अन्य
प्रकाशित: (2011-09-01)

$\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads
द्वारा: Furio Honsell, और अन्य
प्रकाशित: (2017-07-01)

Some model theory for the modal $\mu$-calculus: syntactic characterisations of semantic properties
द्वारा: Gaëlle Fontaine, और अन्य
प्रकाशित: (2018-02-01)

The Completeness of Propositional Resolution: A Simple and Constructive Proof
द्वारा: Jean Gallier
प्रकाशित: (2006-11-01)

Transforming structures by set interpretations
द्वारा: Thomas Colcombet, और अन्य
प्रकाशित: (2007-05-01)

Proof-irrelevant model of CC with predicative induction and judgmental equality
द्वारा: Gyesik Lee, और अन्य
प्रकाशित: (2011-11-01)

Almost periodic functions, constructively
द्वारा: Bas Spitters
प्रकाशित: (2005-12-01)

Algorithmic Randomness and Capacity of Closed Sets
द्वारा: Douglas Cenzer, और अन्य
प्रकाशित: (2011-09-01)

A proof of strong normalisation using domain theory
द्वारा: Thierry Coquand, और अन्य
प्रकाशित: (2007-12-01)

Coalgebraic trace semantics via forgetful logics
द्वारा: Bartek Klin, और अन्य
प्रकाशित: (2017-04-01)

Internalising modified realisability in constructive type theory
द्वारा: Erik Palmgren
प्रकाशित: (2005-10-01)

Realizability algebras: a program to well order R
द्वारा: Jean-Louis Krivine
प्रकाशित: (2011-08-01)

Exhaustible sets in higher-type computation
द्वारा: Martin Escardo
प्रकाशित: (2008-08-01)

On linear rewriting systems for Boolean logic and some applications to proof theory
द्वारा: Anupam Das, और अन्य
प्रकाशित: (2017-04-01)

Width and size of regular resolution proofs
द्वारा: Alasdair Urquhart
प्रकाशित: (2012-06-01)

Game semantics for first-order logic
द्वारा: Olivier Laurent
प्रकाशित: (2010-10-01)

First-order query evaluation on structures of bounded degree
द्वारा: Wojciech Kazana, और अन्य
प्रकाशित: (2011-06-01)

Knowledge-Based Synthesis of Distributed Systems Using Event Structures
द्वारा: Mark Bickford, और अन्य
प्रकाशित: (2011-05-01)

Consistency and Completeness of Rewriting in the Calculus of Constructions
द्वारा: Daria Walukiewicz-Chrzaszcz, और अन्य
प्रकाशित: (2008-09-01)

On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics
द्वारा: Matthias Hoelzel, और अन्य
प्रकाशित: (2021-07-01)

The Algebraic Intersection Type Unification Problem
द्वारा: Andrej Dudenhefner, और अन्य
प्रकाशित: (2017-08-01)

No solvable lambda-value term left behind
द्वारा: Á. García-Pérez, और अन्य
प्रकाशित: (2016-06-01)

Qualitative and Quantitative Monitoring of Spatio-Temporal Properties with SSTL
द्वारा: L. Nenzi, और अन्य
प्रकाशित: (2018-10-01)

Mixin Composition Synthesis based on Intersection Types
द्वारा: Jan Bessai, और अन्य
प्रकाशित: (2018-02-01)

Axioms for Modelling Cubical Type Theory in a Topos
द्वारा: Ian Orton, और अन्य
प्रकाशित: (2018-12-01)

Bounded Linear Logic, Revisited
द्वारा: Ugo Dal Lago, और अन्य
प्रकाशित: (2010-12-01)

Interactive Learning-Based Realizability for Heyting Arithmetic with EM1
द्वारा: Federico Aschieri, और अन्य
प्रकाशित: (2010-09-01)