Volume
LIPIcs, Volume 269
28th International Conference on Types for Proofs and Programs (TYPES 2022)
Publication Details
- published at: 2023-07-28
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-285-3
- DBLP: db/conf/types/types2022
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 269, TYPES 2022, Complete Volume
Abstract
LIPIcs, Volume 269, TYPES 2022, Complete Volume
Cite as
28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 1-342, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Proceedings{kesner_et_al:LIPIcs.TYPES.2022,
title = {{LIPIcs, Volume 269, TYPES 2022, Complete Volume}},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
pages = {1--342},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-285-3},
ISSN = {1868-8969},
year = {2023},
volume = {269},
editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022},
URN = {urn:nbn:de:0030-drops-184425},
doi = {10.4230/LIPIcs.TYPES.2022},
annote = {Keywords: LIPIcs, Volume 269, TYPES 2022, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 0:i-0:viii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{kesner_et_al:LIPIcs.TYPES.2022.0,
author = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
pages = {0:i--0:viii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-285-3},
ISSN = {1868-8969},
year = {2023},
volume = {269},
editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.0},
URN = {urn:nbn:de:0030-drops-184433},
doi = {10.4230/LIPIcs.TYPES.2022.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
All Watched Over by Machines of Loving Grace
Abstract
Modern operating systems are typically built around a trusted system component called the kernel which amongst other things is charged with enforcing system-wide security policies. Crucially, this component must be kept isolated from untrusted software at all times, which is facilitated by exploiting machine-oriented notions of separation: private memories, privilege levels, and similar.
Modern proof-assistants are typically built around a trusted system component called the kernel which is charged with enforcing system-wide soundness. Crucially, this component must be kept isolated from untrusted automation at all times, which is facilitated by exploiting programming-language notions of separation: module-private data structures, type-abstraction, and similar.
Whilst markedly different in purpose, in some essential ways operating system and proof-assistant kernels are tasked with the same job, namely enforcing system-wide invariants in the face of unbridled interaction with untrusted code. Yet the mechanisms through which the two types of kernel protect themselves are significantly different.
In this paper, we introduce Supervisionary, the kernel of a programmable proof-checking system for Gordon’s HOL, organised in a manner more reminiscent of an operating system than a typical LCF-style proof-checker. Supervisionary’s kernel executes at a relative level of privilege compared to untrusted automation, with trusted and untrusted system components communicating across a limited system call boundary. Kernel objects, managed on behalf of user-space by Supervisionary, are referenced by handles and are passed back-and-forth by system calls. Unusually, Supervisionary has no "metalanguage" in the LCF sense, as the language used to implement the kernel, and the language used to implement automation, need not be the same. Any programming language can be used to implement automation for Supervisionary, providing the resulting binary respects the kernel calling convention and binary interface, with no risk to system soundness. Lastly, Supervisionary allows arbitrary programming languages to be endowed with facilities for proof-checking. Indeed, the handles that Supervisionary uses to denote kernel objects may be thought of as an extremely expressive form of capability - in the computer security sense of that word - and can potentially be used to enforce fine-grained correctness and security properties of programs at runtime.
Cite as
Dominic P. Mulligan. All Watched Over by Machines of Loving Grace. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 1:1-1:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{mulligan:LIPIcs.TYPES.2022.1,
author = {Mulligan, Dominic P.},
title = {{All Watched Over by Machines of Loving Grace}},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
pages = {1:1--1:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-285-3},
ISSN = {1868-8969},
year = {2023},
volume = {269},
editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.1},
URN = {urn:nbn:de:0030-drops-184449},
doi = {10.4230/LIPIcs.TYPES.2022.1},
annote = {Keywords: Proof assistant design, operating systems, HOL, LCF, Supervisionary, system description, capabilities}
}
Document
Classical Natural Deduction from Truth Tables
Abstract
In earlier articles we have introduced truth table natural deduction which allows one to extract natural deduction rules for a propositional logic connective from its truth table definition. This works for both intuitionistic logic and classical logic. We have studied the proof theory of the intuitionistic rules in detail, giving rise to a general Kripke semantics and general proof term calculus with reduction rules that are strongly normalizing. In the present paper we study the classical rules and give a term interpretation to classical deductions with reduction rules. As a variation we define a multi-conclusion variant of the natural deduction rules as it simplifies the study of proof term reduction. We show that the reduction is normalizing and gives rise to the sub-formula property. We also compare the logical strength of the classical rules with the intuitionistic ones and we show that if one non-monotone connective is classical, then all connectives become classical.
Cite as
Herman Geuvers and Tonny Hurkens. Classical Natural Deduction from Truth Tables. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 2:1-2:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{geuvers_et_al:LIPIcs.TYPES.2022.2,
author = {Geuvers, Herman and Hurkens, Tonny},
title = {{Classical Natural Deduction from Truth Tables}},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
pages = {2:1--2:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-285-3},
ISSN = {1868-8969},
year = {2023},
volume = {269},
editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.2},
URN = {urn:nbn:de:0030-drops-184450},
doi = {10.4230/LIPIcs.TYPES.2022.2},
annote = {Keywords: Natural deduction, classical proposition logic, multiple conclusion natural deduction, proof terms, formulas-as-types, proof normalization, subformula property, Curry-Howard isomorphism}
}
Document
On Dynamic Lifting and Effect Typing in Circuit Description Languages
Abstract
In the realm of quantum computing, circuit description languages represent a valid alternative to traditional QRAM-style languages. They indeed allow for finer control over the output circuit, without sacrificing flexibility nor modularity. We introduce a generalization of the paradigmatic lambda-calculus Proto-Quipper-M, which models the core features of the quantum circuit description language Quipper. The extension, called Proto-Quipper-K, is meant to capture a very general form of dynamic lifting. This is made possible by the introduction of a rich type and effect system in which not only computations, but also the very types are effectful. The main results we give for the introduced language are the classic type soundness results, namely subject reduction and progress.
Cite as
Andrea Colledan and Ugo Dal Lago. On Dynamic Lifting and Effect Typing in Circuit Description Languages. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{colledan_et_al:LIPIcs.TYPES.2022.3,
author = {Colledan, Andrea and Dal Lago, Ugo},
title = {{On Dynamic Lifting and Effect Typing in Circuit Description Languages}},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
pages = {3:1--3:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-285-3},
ISSN = {1868-8969},
year = {2023},
volume = {269},
editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.3},
URN = {urn:nbn:de:0030-drops-184468},
doi = {10.4230/LIPIcs.TYPES.2022.3},
annote = {Keywords: Circuit-Description Languages, \lambda-calculus, Dynamic lifting, Type and effect systems}
}
Document
Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory
Abstract
Systems in which classical and intuitionistic logics coexist are called ecumenical. Such a system allows for interoperability and hybridization between classical and constructive propositions and proofs. We study Ecumenical STT, a theory expressed in the logical framework of the λΠ-calculus modulo theory. We prove soudness and conservativity of four subtheories of Ecumenical STT with respect to constructive and classical predicate logic and simple type theory. We also prove the weak normalization of well-typed terms and thus the consistency of Ecumenical STT.
Cite as
Emilie Grienenberger. Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{grienenberger:LIPIcs.TYPES.2022.4,
author = {Grienenberger, Emilie},
title = {{Expressing Ecumenical Systems in the \lambda\Pi-Calculus Modulo Theory}},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
pages = {4:1--4:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-285-3},
ISSN = {1868-8969},
year = {2023},
volume = {269},
editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.4},
URN = {urn:nbn:de:0030-drops-184479},
doi = {10.4230/LIPIcs.TYPES.2022.4},
annote = {Keywords: dependent types, predicate logic, higher order logic, constructivism, interoperability, ecumenical logics}
}
Document
On the Fair Termination of Client-Server Sessions
Abstract
Client-server sessions are based on a variation of the traditional interpretation of linear logic propositions as session types in which non-linear channels (those regulating the interaction between a pool of clients and a single server) are typed by coexponentials instead of the usual exponentials. Coexponentials enable the modeling of racing interactions, whereby clients compete to interact with a single server whose internal state (and thus the offered service) may change as the server processes requests sequentially. In this work we present a fair termination result for CSLL^∞, a core calculus of client-server sessions. We design a type system such that every well-typed term corresponds to a valid derivation in μMALL^∞, the infinitary proof theory of linear logic with least and greatest fixed points. We then establish a correspondence between reductions in the calculus and principal reductions in μMALL^∞. Fair termination in CSLL^∞ follows from cut elimination in μMALL^∞.
Cite as
Luca Padovani. On the Fair Termination of Client-Server Sessions. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{padovani:LIPIcs.TYPES.2022.5,
author = {Padovani, Luca},
title = {{On the Fair Termination of Client-Server Sessions}},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
pages = {5:1--5:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-285-3},
ISSN = {1868-8969},
year = {2023},
volume = {269},
editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.5},
URN = {urn:nbn:de:0030-drops-184485},
doi = {10.4230/LIPIcs.TYPES.2022.5},
annote = {Keywords: client-server sessions, linear logic, fixed points, fair termination, cut elimination}
}
Document
{mitten}: A Flexible Multimodal Proof Assistant
Abstract
Recently, there has been a growing interest in type theories which include modalities, unary type constructors which need not commute with substitution. Here we focus on MTT [Daniel Gratzer et al., 2021], a general modal type theory which can internalize arbitrary collections of (dependent) right adjoints [Birkedal et al., 2020]. These modalities are specified by mode theories [Licata and Shulman, 2016], 2-categories whose objects corresponds to modes, morphisms to modalities, and 2-cells to natural transformations between modalities. We contribute a defunctionalized NbE algorithm which reduces the type-checking problem for MTT to deciding the word problem for the mode theory. The algorithm is restricted to the class of preordered mode theories - mode theories with at most one 2-cell between any pair of modalities. Crucially, the normalization algorithm does not depend on the particulars of the mode theory and can be applied without change to any preordered collection of modalities. Furthermore, we specify a bidirectional syntax for MTT together with a type-checking algorithm. We further contribute mitten, a flexible experimental proof assistant implementing these algorithms which supports all decidable preordered mode theories without alteration.
Cite as
Philipp Stassen, Daniel Gratzer, and Lars Birkedal. {mitten}: A Flexible Multimodal Proof Assistant. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{stassen_et_al:LIPIcs.TYPES.2022.6,
author = {Stassen, Philipp and Gratzer, Daniel and Birkedal, Lars},
title = {{\{mitten\}: A Flexible Multimodal Proof Assistant}},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
pages = {6:1--6:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-285-3},
ISSN = {1868-8969},
year = {2023},
volume = {269},
editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.6},
URN = {urn:nbn:de:0030-drops-184498},
doi = {10.4230/LIPIcs.TYPES.2022.6},
annote = {Keywords: Dependent type theory, guarded recursion, modal type theory, proof assistants}
}
Document
An Irrelevancy-Eliminating Translation of Pure Type Systems
Abstract
I present an infinite-reduction-path-preserving typability-preserving translation of pure type systems which eliminates rules and sorts that are in some sense irrelevant with respect to normalization. This translation can be bootstrapped with existing results for the Barendregt-Geuvers-Klop conjecture, extending the conjecture to a larger class of systems. Performing this bootstrapping with the results of Barthe et al. [Barthe et al., 2001] yields a new class of systems with dependent rules and non-negatable sorts for which the conjecture holds. To my knowledge, this is the first improvement in the state of the conjecture since the results of Roux and van Doorn [Roux and Doorn, 2014] (which can be used for the same sort of bootstrapping argument) albeit a somewhat modest one; in essence, the translation eliminates clutter in the system that does not affect normalization. This work is done in the framework of tiered pure type systems, a simple class of persistent systems which is sufficient to study when concerned with questions about normalization.
Cite as
Nathan Mull. An Irrelevancy-Eliminating Translation of Pure Type Systems. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 7:1-7:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{mull:LIPIcs.TYPES.2022.7,
author = {Mull, Nathan},
title = {{An Irrelevancy-Eliminating Translation of Pure Type Systems}},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
pages = {7:1--7:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-285-3},
ISSN = {1868-8969},
year = {2023},
volume = {269},
editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.7},
URN = {urn:nbn:de:0030-drops-184501},
doi = {10.4230/LIPIcs.TYPES.2022.7},
annote = {Keywords: pure type systems, normalization, reduction-path-preserving translations, Barendregt-Geuvers-Klop conjecture}
}
Document
Linear Rank Intersection Types
Abstract
Non-idempotent intersection types provide quantitative information about typed programs, and have been used to obtain time and space complexity measures. Intersection type systems characterize termination, so restrictions need to be made in order to make typability decidable. One such restriction consists in using a notion of finite rank for the idempotent intersection types. In this work, we define a new notion of rank for the non-idempotent intersection types. We then define a novel type system and a type inference algorithm for the λ-calculus, using the new notion of rank 2. In the second part of this work, we extend the type system and the type inference algorithm to use the quantitative properties of the non-idempotent intersection types to infer quantitative information related to resource usage.
Cite as
Fábio Reis, Sandra Alves, and Mário Florido. Linear Rank Intersection Types. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 8:1-8:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{reis_et_al:LIPIcs.TYPES.2022.8,
author = {Reis, F\'{a}bio and Alves, Sandra and Florido, M\'{a}rio},
title = {{Linear Rank Intersection Types}},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
pages = {8:1--8:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-285-3},
ISSN = {1868-8969},
year = {2023},
volume = {269},
editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.8},
URN = {urn:nbn:de:0030-drops-184513},
doi = {10.4230/LIPIcs.TYPES.2022.8},
annote = {Keywords: Lambda-Calculus, Intersection Types, Quantitative Types, Tight Typings}
}
Document
A Metatheoretic Analysis of Subtype Universes
Abstract
Subtype universes were initially introduced as an expressive mechanisation of bounded quantification extending a modern type theory. In this paper, we consider a dependent type theory equipped with coercive subtyping and a generalisation of subtype universes. We prove results regarding the metatheoretic properties of subtype universes, such as consistency and strong normalisation. We analyse the causes of undecidability in bounded quantification, and discuss how coherency impacts the metatheoretic properties of theories implementing bounded quantification. We describe the effects of certain choices of subtyping inference rules on the expressiveness of a type theory, and examine various applications in natural language semantics, programming languages, and mathematics formalisation.
Cite as
Felix Bradley and Zhaohui Luo. A Metatheoretic Analysis of Subtype Universes. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{bradley_et_al:LIPIcs.TYPES.2022.9,
author = {Bradley, Felix and Luo, Zhaohui},
title = {{A Metatheoretic Analysis of Subtype Universes}},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
pages = {9:1--9:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-285-3},
ISSN = {1868-8969},
year = {2023},
volume = {269},
editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.9},
URN = {urn:nbn:de:0030-drops-184520},
doi = {10.4230/LIPIcs.TYPES.2022.9},
annote = {Keywords: Type theory, coercive subtyping, subtype universes}
}
Document
The Münchhausen Method in Type Theory
Abstract
In one of his long tales, after falling into a swamp, Baron Münchhausen salvaged himself and the horse by lifting them both up by his hair. Inspired by this, the paper presents a technique to justify very dependent types. Such types reference the term that they classify, e.g. x : F x. While in most type theories this is not allowed, we propose a technique on salvaging the meaning of both the term and the type. The proposed technique does not refer to preterms or typing relations and works in a completely algebraic setting, e.g categories with families. With a series of examples we demonstrate our technique. We use Agda to demonstrate that our examples are implementable within a proof assistant.
Cite as
Thorsten Altenkirch, Ambrus Kaposi, Artjoms Šinkarovs, and Tamás Végh. The Münchhausen Method in Type Theory. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{altenkirch_et_al:LIPIcs.TYPES.2022.10,
author = {Altenkirch, Thorsten and Kaposi, Ambrus and \v{S}inkarovs, Artjoms and V\'{e}gh, Tam\'{a}s},
title = {{The M\"{u}nchhausen Method in Type Theory}},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
pages = {10:1--10:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-285-3},
ISSN = {1868-8969},
year = {2023},
volume = {269},
editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.10},
URN = {urn:nbn:de:0030-drops-184534},
doi = {10.4230/LIPIcs.TYPES.2022.10},
annote = {Keywords: type theory, proof assistants, very dependent types}
}
Document
Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families
Abstract
There are several ways to formally represent families of data, such as lambda terms, in a type theory such as the dependent type theory of Coq. Mathematical representations are very compact ones and usually rely on the use of dependent types, but they tend to be difficult to handle in practice. On the contrary, implementations based on a larger (and simpler) data structure combined with a restriction property are much easier to deal with.
In this work, we study several families related to lambda terms, among which Motzkin trees, seen as lambda term skeletons, closable Motzkin trees, corresponding to closed lambda terms, and a parameterized family of open lambda terms. For each of these families, we define two different representations, show that they are isomorphic and provide tools to switch from one representation to another. All these datatypes and their associated transformations are implemented in the Coq proof assistant. Furthermore we implement random generators for each representation, using the QuickChick plugin.
Cite as
Catherine Dubois, Nicolas Magaud, and Alain Giorgetti. Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{dubois_et_al:LIPIcs.TYPES.2022.11,
author = {Dubois, Catherine and Magaud, Nicolas and Giorgetti, Alain},
title = {{Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families}},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
pages = {11:1--11:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-285-3},
ISSN = {1868-8969},
year = {2023},
volume = {269},
editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.11},
URN = {urn:nbn:de:0030-drops-184548},
doi = {10.4230/LIPIcs.TYPES.2022.11},
annote = {Keywords: Data Representations, Isomorphisms, dependent Types, formal Proofs, random Generation, lambda Terms, Coq}
}
Document
A Semantics of 𝕂 into Dedukti
Abstract
𝕂 is a semantical framework for formally describing the semantics of programming languages thanks to a BNF grammar and rewriting rules on configurations. It is also an environment that offers various tools to help programming with the languages specified in the formalism. For example, it is possible to execute programs thanks to the generated interpreter, or to check their properties thanks to the provided automatic theorem prover called the KProver. 𝕂 is based on la Matching Logic, a first-order logic with an application and fixed-point operators, extended with symbols to encode equality, typing and rewriting. This specific la Matching Logic theory is called Kore.
Dedukti is a logical framework having for main goal the interoperability of proofs between different formal proof tools. Several translators to Dedukti exist or are under development, in order to automatically translate formalizations written, for instance, in Coq or PVS. Dedukti is based on the λΠ-calculus modulo theory, a λ-calculus with dependent types and extended with a primitive notion of computation defined by rewriting rules. The flexibility of this logical framework allows to encode many theories ranging from first-order logic to the Calculus of Constructions.
In this article, we present a paper formalization of the translation from 𝕂 into Kore, and a paper formalization and an automatic translation tool, called KaMeLo, from Kore to Dedukti in order to execute programs in Dedukti.
Cite as
Amélie Ledein, Valentin Blot, and Catherine Dubois. A Semantics of 𝕂 into Dedukti. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 12:1-12:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{ledein_et_al:LIPIcs.TYPES.2022.12,
author = {Ledein, Am\'{e}lie and Blot, Valentin and Dubois, Catherine},
title = {{A Semantics of \mathbb{K} into Dedukti}},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
pages = {12:1--12:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-285-3},
ISSN = {1868-8969},
year = {2023},
volume = {269},
editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.12},
URN = {urn:nbn:de:0030-drops-184557},
doi = {10.4230/LIPIcs.TYPES.2022.12},
annote = {Keywords: Programming language, Semantics, Rewriting, Logical framework, Type theory}
}
Document
Type Theory with Explicit Universe Polymorphism
Abstract
The aim of this paper is to refine and extend proposals by Sozeau and Tabareau and by Voevodsky for universe polymorphism in type theory. In those systems judgments can depend on explicit constraints between universe levels. We here present a system where we also have products indexed by universe levels and by constraints. Our theory has judgments for internal universe levels, built up from level variables by a successor operation and a binary supremum operation, and also judgments for equality of universe levels.
Cite as
Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó. Type Theory with Explicit Universe Polymorphism. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{bezem_et_al:LIPIcs.TYPES.2022.13,
author = {Bezem, Marc and Coquand, Thierry and Dybjer, Peter and Escard\'{o}, Mart{\'\i}n},
title = {{Type Theory with Explicit Universe Polymorphism}},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
pages = {13:1--13:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-285-3},
ISSN = {1868-8969},
year = {2023},
volume = {269},
editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.13},
URN = {urn:nbn:de:0030-drops-184564},
doi = {10.4230/LIPIcs.TYPES.2022.13},
annote = {Keywords: type theory, universes in type theory, universe polymorphism, level-indexed products, constraint-indexed products}
}
Document
A Univalent Formalization of Constructive Affine Schemes
Abstract
We present a formalization of constructive affine schemes in the Cubical Agda proof assistant. This development is not only fully constructive and predicative, it also makes crucial use of univalence. By now schemes have been formalized in various proof assistants. However, most existing formalizations follow the inherently non-constructive approach of Hartshorne’s classic "Algebraic Geometry" textbook, for which the construction of the so-called structure sheaf is rather straightforwardly formalizable and works the same with or without univalence. We follow an alternative approach that uses a point-free description of the constructive counterpart of the Zariski spectrum called the Zariski lattice and proceeds by defining the structure sheaf on formal basic opens and then lift it to the whole lattice. This general strategy is used in a plethora of textbooks, but formalizing it has proved tricky. The main result of this paper is that with the help of the univalence principle we can make this "lift from basis" strategy formal and obtain a fully formalized account of constructive affine schemes.
Cite as
Max Zeuner and Anders Mörtberg. A Univalent Formalization of Constructive Affine Schemes. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 14:1-14:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{zeuner_et_al:LIPIcs.TYPES.2022.14,
author = {Zeuner, Max and M\"{o}rtberg, Anders},
title = {{A Univalent Formalization of Constructive Affine Schemes}},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
pages = {14:1--14:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-285-3},
ISSN = {1868-8969},
year = {2023},
volume = {269},
editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.14},
URN = {urn:nbn:de:0030-drops-184574},
doi = {10.4230/LIPIcs.TYPES.2022.14},
annote = {Keywords: Affine Schemes, Homotopy Type Theory and Univalent Foundations, Cubical Agda, Constructive Mathematics}
}
Document
Univalent Monoidal Categories
Abstract
Univalent categories constitute a well-behaved and useful notion of category in univalent foundations. The notion of univalence has subsequently been generalized to bicategories and other structures in (higher) category theory. Here, we zoom in on monoidal categories and study them in a univalent setting. Specifically, we show that the bicategory of univalent monoidal categories is univalent. Furthermore, we construct a Rezk completion for monoidal categories: we show how any monoidal category is weakly equivalent to a univalent monoidal category, universally. We have fully formalized these results in UniMath, a library of univalent mathematics in the Coq proof assistant.
Cite as
Kobe Wullaert, Ralph Matthes, and Benedikt Ahrens. Univalent Monoidal Categories. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 15:1-15:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{wullaert_et_al:LIPIcs.TYPES.2022.15,
author = {Wullaert, Kobe and Matthes, Ralph and Ahrens, Benedikt},
title = {{Univalent Monoidal Categories}},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
pages = {15:1--15:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-285-3},
ISSN = {1868-8969},
year = {2023},
volume = {269},
editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.15},
URN = {urn:nbn:de:0030-drops-184580},
doi = {10.4230/LIPIcs.TYPES.2022.15},
annote = {Keywords: Univalence, Monoidal categories, Rezk completion, Displayed (bi)categories, Proof assistant Coq, UniMath library}
}