Volume
LIPIcs, Volume 188
26th International Conference on Types for Proofs and Programs (TYPES 2020)
Event
TYPES 2020, March 2-5, 2020, University of Turin, ItalyEditors
Publication Details
- published at: 2021-06-07
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-182-5
- DBLP: db/conf/types/types2020
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 188, TYPES 2020, Complete Volume
Abstract
LIPIcs, Volume 188, TYPES 2020, Complete Volume
Cite as
26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 1-204, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@Proceedings{deliguoro_et_al:LIPIcs.TYPES.2020,
title = {{LIPIcs, Volume 188, TYPES 2020, Complete Volume}},
booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)},
pages = {1--204},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-182-5},
ISSN = {1868-8969},
year = {2021},
volume = {188},
editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020},
URN = {urn:nbn:de:0030-drops-138785},
doi = {10.4230/LIPIcs.TYPES.2020},
annote = {Keywords: LIPIcs, Volume 188, TYPES 2020, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 0:i-0:viii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{deliguoro_et_al:LIPIcs.TYPES.2020.0,
author = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)},
pages = {0:i--0:viii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-182-5},
ISSN = {1868-8969},
year = {2021},
volume = {188},
editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.0},
URN = {urn:nbn:de:0030-drops-138792},
doi = {10.4230/LIPIcs.TYPES.2020.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction
Abstract
Intuitionistic truth table natural deduction (ITTND) by Geuvers and Hurkens (2017), which is inherently non-confluent, has been shown strongly normalizing (SN) using continuation-passing-style translations to parallel lambda calculus by Geuvers, van der Giessen, and Hurkens (2019). We investigate the applicability of standard model-theoretic proof techniques and show (1) SN of detour reduction (β) using Girard’s reducibility candidates, and (2) SN of detour and permutation reduction (βπ) using biorthogonals. In the appendix, we adapt Tait’s method of saturated sets to β, clarifying the original proof of 2017, and extend it to βπ.
Cite as
Andreas Abel. On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{abel:LIPIcs.TYPES.2020.1,
author = {Abel, Andreas},
title = {{On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction}},
booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)},
pages = {1:1--1:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-182-5},
ISSN = {1868-8969},
year = {2021},
volume = {188},
editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.1},
URN = {urn:nbn:de:0030-drops-138805},
doi = {10.4230/LIPIcs.TYPES.2020.1},
annote = {Keywords: Natural deduction, Permutative conversion, Reducibility, Strong normalization, Truth table}
}
Document
Extending Equational Monadic Reasoning with Monad Transformers
Abstract
There is a recent interest for the verification of monadic programs using proof assistants. This line of research raises the question of the integration of monad transformers, a standard technique to combine monads. In this paper, we extend Monae, a Coq library for monadic equational reasoning, with monad transformers and we explain the benefits of this extension. Our starting point is the existing theory of modular monad transformers, which provides a uniform treatment of operations. Using this theory, we simplify the formalization of models in Monae and we propose an approach to support monadic equational reasoning in the presence of monad transformers. We also use Monae to revisit the lifting theorems of modular monad transformers by providing equational proofs and explaining how to patch a known bug using a non-standard use of Coq that combines impredicative polymorphism and parametricity.
Cite as
Reynald Affeldt and David Nowak. Extending Equational Monadic Reasoning with Monad Transformers. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 2:1-2:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{affeldt_et_al:LIPIcs.TYPES.2020.2,
author = {Affeldt, Reynald and Nowak, David},
title = {{Extending Equational Monadic Reasoning with Monad Transformers}},
booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)},
pages = {2:1--2:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-182-5},
ISSN = {1868-8969},
year = {2021},
volume = {188},
editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.2},
URN = {urn:nbn:de:0030-drops-138810},
doi = {10.4230/LIPIcs.TYPES.2020.2},
annote = {Keywords: monads, monad transformers, Coq, impredicativity, parametricity}
}
Document
Towards a Certified Reference Monitor of the Android 10 Permission System
Abstract
Android is a platform for mobile devices that captures more than 85% of the total market share [International Data Corporation (IDC), 2020]. Currently, mobile devices allow people to develop multiple tasks in different areas. Regrettably, the benefits of using mobile devices are counteracted by increasing security risks. The important and critical role of these systems makes them a prime target for formal verification. In our previous work [Betarte et al., 2018], we exhibited a formal specification of an idealized formulation of the permission model of version 6 of Android. In this paper we present an enhanced version of the model in the proof assistant Coq, including the most relevant changes concerning the permission system introduced in versions Nougat, Oreo, Pie and 10. The properties that we had proved earlier for the security model have been either revalidated or refuted, and new ones have been formulated and proved. Additionally, we make observations on the security of the most recent versions of Android. Using the programming language of Coq we have developed a functional implementation of a reference validation mechanism and certified its correctness. The formal development is about 23k LOC of Coq, including proofs.
Cite as
Guido De Luca and Carlos Luna. Towards a Certified Reference Monitor of the Android 10 Permission System. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{deluca_et_al:LIPIcs.TYPES.2020.3,
author = {De Luca, Guido and Luna, Carlos},
title = {{Towards a Certified Reference Monitor of the Android 10 Permission System}},
booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)},
pages = {3:1--3:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-182-5},
ISSN = {1868-8969},
year = {2021},
volume = {188},
editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.3},
URN = {urn:nbn:de:0030-drops-138821},
doi = {10.4230/LIPIcs.TYPES.2020.3},
annote = {Keywords: Android, Permission model, Formal idealized model, Reference monitor, Formal proofs, Certified implementation, Coq}
}
Document
Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic
Abstract
The approach to proof search dubbed "coinductive proof search", and previously developed by the authors for implicational intuitionistic logic, is in this paper extended to LJP, a focused sequent-calculus presentation of polarized intuitionistic logic, including an array of positive and negative connectives. As before, this includes developing a coinductive description of the search space generated by a sequent, an equivalent inductive syntax describing the same space, and decision procedures for inhabitation problems in the form of predicates defined by recursion on the inductive syntax. We prove the decidability of existence of focused inhabitants, and of finiteness of the number of focused inhabitants for polarized intuitionistic logic, by means of such recursive procedures. Moreover, the polarized logic can be used as a platform from which proof search for other logics is understood. We illustrate the technique with LJT, a focused sequent calculus for full intuitionistic propositional logic (including disjunction). For that, we have to work out the "negative translation" of LJT into LJP (that sees all intuitionistic types as negative types), and verify that the translation gives a faithful representation of proof search in LJT as proof search in the polarized logic. We therefore inherit decidability of both problems studied for LJP and thus get new proofs of these results for LJT.
Cite as
José Espírito Santo, Ralph Matthes, and Luís Pinto. Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 4:1-4:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{espiritosanto_et_al:LIPIcs.TYPES.2020.4,
author = {Esp{\'\i}rito Santo, Jos\'{e} and Matthes, Ralph and Pinto, Lu{\'\i}s},
title = {{Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic}},
booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)},
pages = {4:1--4:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-182-5},
ISSN = {1868-8969},
year = {2021},
volume = {188},
editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.4},
URN = {urn:nbn:de:0030-drops-138837},
doi = {10.4230/LIPIcs.TYPES.2020.4},
annote = {Keywords: Inhabitation problems, Coinduction, Lambda-calculus, Polarized logic}
}
Document
Synthetic Completeness for a Terminating Seligman-Style Tableau System
Abstract
Hybrid logic extends modal logic with nominals that name worlds. Seligman-style tableau systems for hybrid logic divide branches into blocks named by nominals to achieve a local proof style. We present a Seligman-style tableau system with a formalization in the proof assistant Isabelle/HOL. Our system refines an existing system to simplify formalization and we claim termination from this relationship. Existing completeness proofs that account for termination are either analytic or based on translation, but synthetic proofs have been shown to generalize to richer logics and languages. Our main result is the first synthetic completeness proof for a terminating hybrid logic tableau system. It is also the first formalized completeness proof for any hybrid logic proof system.
Cite as
Asta Halkjær From. Synthetic Completeness for a Terminating Seligman-Style Tableau System. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{from:LIPIcs.TYPES.2020.5,
author = {From, Asta Halkj{\ae}r},
title = {{Synthetic Completeness for a Terminating Seligman-Style Tableau System}},
booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)},
pages = {5:1--5:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-182-5},
ISSN = {1868-8969},
year = {2021},
volume = {188},
editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.5},
URN = {urn:nbn:de:0030-drops-138847},
doi = {10.4230/LIPIcs.TYPES.2020.5},
annote = {Keywords: Hybrid logic, Seligman-style tableau, synthetic completeness, Isabelle/HOL}
}
Document
Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory
Abstract
The λΠ-calculus modulo theory is a logical framework in which various logics and type systems can be encoded, thus helping the cross-verification and interoperability of proof systems based on those logics and type systems. In this paper, we show how to encode predicate subtyping and proof irrelevance, two important features of the PVS proof assistant. We prove that this encoding is correct and that encoded proofs can be mechanically checked by Dedukti, a type checker for the λΠ-calculus modulo theory using rewriting.
Cite as
Gabriel Hondet and Frédéric Blanqui. Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{hondet_et_al:LIPIcs.TYPES.2020.6,
author = {Hondet, Gabriel and Blanqui, Fr\'{e}d\'{e}ric},
title = {{Encoding of Predicate Subtyping with Proof Irrelevance in the \lambda\Pi-Calculus Modulo Theory}},
booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)},
pages = {6:1--6:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-182-5},
ISSN = {1868-8969},
year = {2021},
volume = {188},
editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.6},
URN = {urn:nbn:de:0030-drops-138853},
doi = {10.4230/LIPIcs.TYPES.2020.6},
annote = {Keywords: Predicate Subtyping, Logical Framework, PVS, Dedukti, Proof Irrelevance}
}
Document
Λ-Symsym: An Interactive Tool for Playing with Involutions and Types
Abstract
We present the web portal Λ-symsym, available at http://158.110.146.197:31780/automata/, for experimenting with game semantics of λ^!-calculus, and its normalizing elementary sub-calculus, the λ^{EAL}-calculus. The λ^!-calculus is a generalization of the λ-calculus obtained by introducing a modal operator !, giving rise to a pattern β-reduction. Its sub-calculus corresponds to an applicatively closed class of terms normalizing in an elementary number of steps, in which all elementary functions can be encoded. The game model which we consider is the Geometry of Interaction model I introduced by Abramsky to study reversible computations, consisting of partial involutions over a very simple language of moves.
Given a λ^!- or a λ^{EAL}-term, M, Λ-symsym provides:
- an abstraction algorithm A^!, for compiling M into a term, A^!(M), of the linear combinatory logic CL^{!}, or the normalizing combinatory logic CL^{EAL};
- an interpretation algorithm [[ ]]^I yielding a specification of the partial involution [[A^!(M)]]^I in the model I;
- an algorithm, I2T, for synthesizing from [[A^!(M)]]^I a type, I2T([[A^!(M)]]^I), in a multimodal, intersection type assignment discipline, ⊢_!.
- an algorithm, T2I, for synthesizing a specification of a partial involution from a type in ⊢_!, which is an inverse to the former. We conjecture that ⊢_! M : I2T([[A^!(M)]]^I). Λ-symsym permits to investigate experimentally the fine structure of I, and hence the game semantics of the λ^!- and λ^{EAL}-calculi. For instance, we can easily verify that the model I is a λ^!-algebra in the case of strictly linear λ-terms, by checking all the necessary equations, and find counterexamples in the general case.
We make this tool available for readers interested to play with games (-semantics). The paper builds on earlier work by the authors, the type system being an improvement.
Cite as
Furio Honsell, Marina Lenisa, and Ivan Scagnetto. Λ-Symsym: An Interactive Tool for Playing with Involutions and Types. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{honsell_et_al:LIPIcs.TYPES.2020.7,
author = {Honsell, Furio and Lenisa, Marina and Scagnetto, Ivan},
title = {{\Lambda-Symsym: An Interactive Tool for Playing with Involutions and Types}},
booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)},
pages = {7:1--7:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-182-5},
ISSN = {1868-8969},
year = {2021},
volume = {188},
editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.7},
URN = {urn:nbn:de:0030-drops-138867},
doi = {10.4230/LIPIcs.TYPES.2020.7},
annote = {Keywords: game semantics, lambda calculus, involutions, linear logic, implicit computational complexity}
}
Document
Why Not W?
Abstract
In an extensional setting, 𝚆 types are sufficient to construct a broad class of inductive types, but in intensional type theory the standard construction of even the natural numbers does not satisfy the required induction principle. In this paper, we show how to refine the standard construction of inductive types such that the induction principle is provable and computes as expected in intensional type theory without using function extensionality. We extend this by constructing from 𝚆 an internal universe of codes for inductive types, such that this universe is itself an inductive type described by a code in the next larger universe. We use this universe to mechanize and internalize our refined construction.
Cite as
Jasper Hugunin. Why Not W?. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 8:1-8:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{hugunin:LIPIcs.TYPES.2020.8,
author = {Hugunin, Jasper},
title = {{Why Not W?}},
booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)},
pages = {8:1--8:9},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-182-5},
ISSN = {1868-8969},
year = {2021},
volume = {188},
editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.8},
URN = {urn:nbn:de:0030-drops-138876},
doi = {10.4230/LIPIcs.TYPES.2020.8},
annote = {Keywords: dependent types, intensional type theory, inductive types, W types}
}
Document
Subtype Universes
Abstract
We introduce a new concept called a subtype universe, which is a collection of subtypes of a particular type. Amongst other things, subtype universes can model bounded quantification without undecidability. Subtype universes have applications in programming, formalisation and natural language semantics. Our construction builds on coercive subtyping, a system of subtyping that preserves canonicity. We prove Strong Normalisation, Subject Reduction and Logical Consistency for our system via transfer from its parent system UTT[ℂ]. We discuss the interaction between subtype universes and other sorts of universe and compare our construction to previous work on Power types.
Cite as
Harry Maclean and Zhaohui Luo. Subtype Universes. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{maclean_et_al:LIPIcs.TYPES.2020.9,
author = {Maclean, Harry and Luo, Zhaohui},
title = {{Subtype Universes}},
booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)},
pages = {9:1--9:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-182-5},
ISSN = {1868-8969},
year = {2021},
volume = {188},
editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.9},
URN = {urn:nbn:de:0030-drops-138880},
doi = {10.4230/LIPIcs.TYPES.2020.9},
annote = {Keywords: Type theory, coercive subtyping, subtype universe}
}
Document
Two Applications of Logic Programming to Coq
Abstract
The logic programming paradigm provides a flexible setting for representing, manipulating, checking, and elaborating proof structures. This is particularly true when the logic programming language allows for bindings in terms and proofs. In this paper, we make use of two recent innovations at the intersection of logic programming and proof checking. One of these is the foundational proof certificate (FPC) framework which provides a flexible means of defining the semantics of a range of proof structures for classical and intuitionistic logic. A second innovation is the recently released Coq-Elpi plugin for Coq in which the Elpi implementation of λProlog can send and retrieve information to and from the Coq kernel. We illustrate the use of both this Coq plugin and FPCs with two example applications. First, we implement an FPC-driven sequent calculus for a fragment of the Calculus of Inductive Constructions and we package it into a tactic to perform property-based testing of inductive types corresponding to Horn clauses. Second, we implement in Elpi a proof checker for first-order intuitionistic logic and demonstrate how proof certificates can be supplied by external (to Coq) provers and then elaborated into the fully detailed proof terms that can be checked by the Coq kernel.
Cite as
Matteo Manighetti, Dale Miller, and Alberto Momigliano. Two Applications of Logic Programming to Coq. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{manighetti_et_al:LIPIcs.TYPES.2020.10,
author = {Manighetti, Matteo and Miller, Dale and Momigliano, Alberto},
title = {{Two Applications of Logic Programming to Coq}},
booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)},
pages = {10:1--10:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-182-5},
ISSN = {1868-8969},
year = {2021},
volume = {188},
editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.10},
URN = {urn:nbn:de:0030-drops-138896},
doi = {10.4230/LIPIcs.TYPES.2020.10},
annote = {Keywords: Proof assistants, logic programming, Coq, \lambdaProlog, property-based testing}
}
Document
Duality in Intuitionistic Propositional Logic
Abstract
It is known that provability in propositional intuitionistic logic is Pspace-complete. As Pspace is closed under complements, there must exist a Logspace-reduction from refutability to provability. Here we describe a direct translation: given a formula φ, we define ̅φ so that ̅φ is provable if and only if φ is not.
Cite as
Paweł Urzyczyn. Duality in Intuitionistic Propositional Logic. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 11:1-11:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{urzyczyn:LIPIcs.TYPES.2020.11,
author = {Urzyczyn, Pawe{\l}},
title = {{Duality in Intuitionistic Propositional Logic}},
booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)},
pages = {11:1--11:10},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-182-5},
ISSN = {1868-8969},
year = {2021},
volume = {188},
editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.11},
URN = {urn:nbn:de:0030-drops-138901},
doi = {10.4230/LIPIcs.TYPES.2020.11},
annote = {Keywords: Intuitionistic logic, Complexity}
}