eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-06-07
188
1
204
10.4230/LIPIcs.TYPES.2020
article
LIPIcs, Volume 188, TYPES 2020, Complete Volume
de'Liguoro, Ugo
1
Berardi, Stefano
1
Altenkirch, Thorsten
2
https://orcid.org/0000-0002-6582-5025
University of Turin, Italy
University of Nottingham, UK
LIPIcs, Volume 188, TYPES 2020, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol188-types2020/LIPIcs.TYPES.2020/LIPIcs.TYPES.2020.pdf
LIPIcs, Volume 188, TYPES 2020, Complete Volume
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-06-07
188
0:i
0:viii
10.4230/LIPIcs.TYPES.2020.0
article
Front Matter, Table of Contents, Preface, Conference Organization
de'Liguoro, Ugo
1
Berardi, Stefano
1
Altenkirch, Thorsten
2
https://orcid.org/0000-0002-6582-5025
University of Turin, Italy
University of Nottingham, UK
Front Matter, Table of Contents, Preface, Conference Organization
https://drops.dagstuhl.de/storage/00lipics/lipics-vol188-types2020/LIPIcs.TYPES.2020.0/LIPIcs.TYPES.2020.0.pdf
Front Matter
Table of Contents
Preface
Conference Organization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-06-07
188
1:1
1:21
10.4230/LIPIcs.TYPES.2020.1
article
On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction
Abel, Andreas
1
2
https://orcid.org/0000-0003-0420-4492
Department of Computer Science and Engineering, Chalmers University of Technology, Göteborg, Sweden
Gothenburg University, Göteborg, Sweden
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 βπ.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol188-types2020/LIPIcs.TYPES.2020.1/LIPIcs.TYPES.2020.1.pdf
Natural deduction
Permutative conversion
Reducibility
Strong normalization
Truth table
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-06-07
188
2:1
2:21
10.4230/LIPIcs.TYPES.2020.2
article
Extending Equational Monadic Reasoning with Monad Transformers
Affeldt, Reynald
1
https://orcid.org/0000-0002-2327-953X
Nowak, David
2
National Institute of Advanced Industrial Science and Technology (AIST), Tokyo, Japan
Univ. Lille, CNRS, Centrale Lille, UMR 9189 CRIStAL, F-59000 Lille, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol188-types2020/LIPIcs.TYPES.2020.2/LIPIcs.TYPES.2020.2.pdf
monads
monad transformers
Coq
impredicativity
parametricity
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-06-07
188
3:1
3:18
10.4230/LIPIcs.TYPES.2020.3
article
Towards a Certified Reference Monitor of the Android 10 Permission System
De Luca, Guido
1
Luna, Carlos
2
Universidad Nacional de Rosario, Argentina
InCo, Facultad de Ingeniería, Universidad de la República, Montevideo, Uruguay
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol188-types2020/LIPIcs.TYPES.2020.3/LIPIcs.TYPES.2020.3.pdf
Android
Permission model
Formal idealized model
Reference monitor
Formal proofs
Certified implementation
Coq
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-06-07
188
4:1
4:24
10.4230/LIPIcs.TYPES.2020.4
article
Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic
Espírito Santo, José
1
https://orcid.org/0000-0002-6348-5653
Matthes, Ralph
2
https://orcid.org/0000-0002-7299-2411
Pinto, Luís
1
https://orcid.org/0000-0003-1338-2688
Centre of Mathematics, University of Minho, Braga, Portugal
CNRS, Institut de Recherche en Informatique de Toulouse (IRIT), France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol188-types2020/LIPIcs.TYPES.2020.4/LIPIcs.TYPES.2020.4.pdf
Inhabitation problems
Coinduction
Lambda-calculus
Polarized logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-06-07
188
5:1
5:17
10.4230/LIPIcs.TYPES.2020.5
article
Synthetic Completeness for a Terminating Seligman-Style Tableau System
From, Asta Halkjær
1
https://orcid.org/0000-0002-3601-0804
Technical University of Denmark, Kongens Lyngby, Denmark
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol188-types2020/LIPIcs.TYPES.2020.5/LIPIcs.TYPES.2020.5.pdf
Hybrid logic
Seligman-style tableau
synthetic completeness
Isabelle/HOL
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-06-07
188
6:1
6:18
10.4230/LIPIcs.TYPES.2020.6
article
Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory
Hondet, Gabriel
1
Blanqui, Frédéric
1
https://orcid.org/0000-0001-7438-5554
Université Paris-Saclay, ENS Paris-Saclay, CNRS, Inria, Laboratoire Méthodes Formelles, Gif-sur-Yvette, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol188-types2020/LIPIcs.TYPES.2020.6/LIPIcs.TYPES.2020.6.pdf
Predicate Subtyping
Logical Framework
PVS
Dedukti
Proof Irrelevance
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-06-07
188
7:1
7:18
10.4230/LIPIcs.TYPES.2020.7
article
Λ-Symsym: An Interactive Tool for Playing with Involutions and Types
Honsell, Furio
1
Lenisa, Marina
1
Scagnetto, Ivan
1
University of Udine, Italy
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol188-types2020/LIPIcs.TYPES.2020.7/LIPIcs.TYPES.2020.7.pdf
game semantics
lambda calculus
involutions
linear logic
implicit computational complexity
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-06-07
188
8:1
8:9
10.4230/LIPIcs.TYPES.2020.8
article
Why Not W?
Hugunin, Jasper
1
https://orcid.org/0000-0002-1133-5354
Carnegie Mellon University, Pittsburgh, PA, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol188-types2020/LIPIcs.TYPES.2020.8/LIPIcs.TYPES.2020.8.pdf
dependent types
intensional type theory
inductive types
W types
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-06-07
188
9:1
9:16
10.4230/LIPIcs.TYPES.2020.9
article
Subtype Universes
Maclean, Harry
1
https://orcid.org/0000-0001-5537-7663
Luo, Zhaohui
1
Royal Holloway, University of London, UK
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol188-types2020/LIPIcs.TYPES.2020.9/LIPIcs.TYPES.2020.9.pdf
Type theory
coercive subtyping
subtype universe
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-06-07
188
10:1
10:19
10.4230/LIPIcs.TYPES.2020.10
article
Two Applications of Logic Programming to Coq
Manighetti, Matteo
1
2
Miller, Dale
1
2
Momigliano, Alberto
3
https://orcid.org/0000-0003-0942-4777
Inria, Palaiseau, France
LIX, Ecole Polytechnique, Palaiseau, France
Dipartimento di Informatica, University of Milan, Italy
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol188-types2020/LIPIcs.TYPES.2020.10/LIPIcs.TYPES.2020.10.pdf
Proof assistants
logic programming
Coq
λProlog
property-based testing
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-06-07
188
11:1
11:10
10.4230/LIPIcs.TYPES.2020.11
article
Duality in Intuitionistic Propositional Logic
Urzyczyn, Paweł
1
https://orcid.org/0000-0003-3719-9618
Institute of Informatics, University of Warsaw, Poland
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol188-types2020/LIPIcs.TYPES.2020.11/LIPIcs.TYPES.2020.11.pdf
Intuitionistic logic
Complexity