Volume
LIPIcs, Volume 239
27th International Conference on Types for Proofs and Programs (TYPES 2021)
Publication Details
- published at: 2022-08-04
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-254-9
- DBLP: db/conf/types/types2021
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 239, TYPES 2021, Complete Volume
Abstract
LIPIcs, Volume 239, TYPES 2021, Complete Volume
Cite as
27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 1-280, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Proceedings{basold_et_al:LIPIcs.TYPES.2021,
title = {{LIPIcs, Volume 239, TYPES 2021, Complete Volume}},
booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)},
pages = {1--280},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-254-9},
ISSN = {1868-8969},
year = {2022},
volume = {239},
editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021},
URN = {urn:nbn:de:0030-drops-167680},
doi = {10.4230/LIPIcs.TYPES.2021},
annote = {Keywords: LIPIcs, Volume 239, TYPES 2021, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 0:i-0:viii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{basold_et_al:LIPIcs.TYPES.2021.0,
author = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)},
pages = {0:i--0:viii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-254-9},
ISSN = {1868-8969},
year = {2022},
volume = {239},
editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.0},
URN = {urn:nbn:de:0030-drops-167691},
doi = {10.4230/LIPIcs.TYPES.2021.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control
Abstract
This paper contributes to the verification of programs written in Bitcoin’s smart contract language script in the interactive theorem prover Agda. It focuses on the security property of access control for script programs that govern the distribution of Bitcoins. It advocates that weakest preconditions in the context of Hoare triples are the appropriate notion for verifying access control. It aims at obtaining human-readable descriptions of weakest preconditions in order to close the validation gap between user requirements and formal specification of smart contracts.
As examples for the proposed approach, the paper focuses on two standard script programs that govern the distribution of Bitcoins, Pay to Public Key Hash (P2PKH) and Pay to Multisig (P2MS). The paper introduces an operational semantics of the script commands used in P2PKH and P2MS, which is formalised in the Agda proof assistant and reasoned about using Hoare triples. Two methodologies for obtaining human-readable descriptions of weakest preconditions are discussed: (1) a step-by-step approach, which works backwards instruction by instruction through a script, sometimes grouping several instructions together; (2) symbolic execution of the code and translation into a nested case distinction, which allows to read off weakest preconditions as the disjunction of conjunctions of conditions along accepting paths. A syntax for equational reasoning with Hoare Triples is defined in order to formalise those approaches in Agda.
Cite as
Fahad F. Alhabardi, Arnold Beckmann, Bogdan Lazar, and Anton Setzer. Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 1:1-1:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{alhabardi_et_al:LIPIcs.TYPES.2021.1,
author = {Alhabardi, Fahad F. and Beckmann, Arnold and Lazar, Bogdan and Setzer, Anton},
title = {{Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control}},
booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)},
pages = {1:1--1:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-254-9},
ISSN = {1868-8969},
year = {2022},
volume = {239},
editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.1},
URN = {urn:nbn:de:0030-drops-167704},
doi = {10.4230/LIPIcs.TYPES.2021.1},
annote = {Keywords: Blockchain, Cryptocurrency, Bitcoin, Agda, Verification, Hoare logic, Bitcoin Script, P2PKH, P2MS, Access control, Weakest precondition, Predicate transformer semantics, Provable correctness, Symbolic execution, Smart contracts}
}
Document
Formalisation of Dependent Type Theory: The Example of CaTT
Abstract
We present the type theory CaTT, originally introduced by Finster and Mimram to describe globular weak ω-categories, formalise this theory in the language of homotopy type theory and discuss connections with the open problem internalising higher structures. Most of the studies about this type theory assume that it is well-formed and satisfy the usual syntactic properties that dependent type theories enjoy, without being completely clear and thorough about what these properties are exactly. We use our formalisation to list and formally prove all of these meta-properties, thus filling a gap in the foundational aspect. We discuss the aspects of the formalisation inherent to CaTT. We present the formalisation in a way that not only handles the type theory CaTT but also related type theories that share the same structure, and in particular we show that this formalisation provides a proper ground to the study of the theory MCaTT which describes the globular monoidal weak ω-categories. The article is accompanied by a development in the proof assistant Agda to check the formalisation that we present.
Cite as
Thibaut Benjamin. Formalisation of Dependent Type Theory: The Example of CaTT. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 2:1-2:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{benjamin:LIPIcs.TYPES.2021.2,
author = {Benjamin, Thibaut},
title = {{Formalisation of Dependent Type Theory: The Example of CaTT}},
booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)},
pages = {2:1--2:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-254-9},
ISSN = {1868-8969},
year = {2022},
volume = {239},
editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.2},
URN = {urn:nbn:de:0030-drops-167719},
doi = {10.4230/LIPIcs.TYPES.2021.2},
annote = {Keywords: Dependent type theory, homotopy type theory, higher categories, formalisation, Agda, proof assistant}
}
Document
Strictification of Weakly Stable Type-Theoretic Structures Using Generic Contexts
Abstract
We present a new strictification method for type-theoretic structures that are only weakly stable under substitution. Given weakly stable structures over some model of type theory, we construct equivalent strictly stable structures by evaluating the weakly stable structures at generic contexts. These generic contexts are specified using the categorical notion of familial representability. This generalizes the local universes method of Lumsdaine and Warren.
We show that generic contexts can also be constructed in any category with families which is freely generated by collections of types and terms, without any definitional equality. This relies on the fact that they support first-order unification. These free models can only be equipped with weak type-theoretic structures, whose computation rules are given by typal equalities. Our main result is that any model of type theory with weakly stable weak type-theoretic structures admits an equivalent model with strictly stable weak type-theoretic structures.
Cite as
Rafaël Bocquet. Strictification of Weakly Stable Type-Theoretic Structures Using Generic Contexts. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 3:1-3:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{bocquet:LIPIcs.TYPES.2021.3,
author = {Bocquet, Rafa\"{e}l},
title = {{Strictification of Weakly Stable Type-Theoretic Structures Using Generic Contexts}},
booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)},
pages = {3:1--3:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-254-9},
ISSN = {1868-8969},
year = {2022},
volume = {239},
editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.3},
URN = {urn:nbn:de:0030-drops-167724},
doi = {10.4230/LIPIcs.TYPES.2021.3},
annote = {Keywords: type theory, strictification, coherence, familial representability, unification}
}
Document
A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-Löf Type Theory
Abstract
The Agda Universal Algebra Library is a project aimed at formalizing the foundations of universal algebra, equational logic and model theory in dependent type theory using Agda. In this paper we draw from many components of the library to present a self-contained, formal, constructive proof of Birkhoff’s HSP theorem in Martin-Löf dependent type theory. This achieves one of the project’s initial goals: to demonstrate the expressive power of inductive and dependent types for representing and reasoning about general algebraic and relational structures by using them to formalize a significant theorem in the field.
Cite as
William DeMeo and Jacques Carette. A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-Löf Type Theory. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{demeo_et_al:LIPIcs.TYPES.2021.4,
author = {DeMeo, William and Carette, Jacques},
title = {{A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-L\"{o}f Type Theory}},
booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)},
pages = {4:1--4:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-254-9},
ISSN = {1868-8969},
year = {2022},
volume = {239},
editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.4},
URN = {urn:nbn:de:0030-drops-167737},
doi = {10.4230/LIPIcs.TYPES.2021.4},
annote = {Keywords: Agda, constructive mathematics, dependent types, equational logic, formal verification, Martin-L\"{o}f type theory, model theory, universal algebra}
}
Document
Principal Types as Lambda Nets
Abstract
We show that there are connections between principal type schemata, cut-free λ-nets, and normal forms of the λ-calculus, and hence there are correspondences between the normalisation algorithms of the above structures, i.e. unification of principal types, cut-elimination of λ-nets, and normalisation of λ-terms. Once the above correspondences have been established, properties of the typing system, such as typability, subject reduction, and inhabitation, can be derived from properties of λ-nets, and vice-versa. We illustrate the above pattern on a specific type assignment system, we study principal types for this system, and we show that they correspond to λ-nets with a non-standard notion of cut-elimination. Properties of the type system are then derived from results on λ-nets.
Cite as
Pietro Di Gianantonio and Marina Lenisa. Principal Types as Lambda Nets. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 5:1-5:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{digianantonio_et_al:LIPIcs.TYPES.2021.5,
author = {Di Gianantonio, Pietro and Lenisa, Marina},
title = {{Principal Types as Lambda Nets}},
booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)},
pages = {5:1--5:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-254-9},
ISSN = {1868-8969},
year = {2022},
volume = {239},
editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.5},
URN = {urn:nbn:de:0030-drops-167744},
doi = {10.4230/LIPIcs.TYPES.2021.5},
annote = {Keywords: Lambda calculus, Principal types, Linear logic, Lambda nets, Normalization, Cut elimination}
}
Document
Internal Strict Propositions Using Point-Free Equations
Abstract
The setoid model of Martin-Löf’s type theory bootstraps extensional features of type theory from intensional type theory equipped with a universe of definitionally proof irrelevant (strict) propositions. Extensional features include a Prop-valued identity type with a strong transport rule and function extensionality. We show that a setoid model supporting these features can be defined in intensional type theory without any of these features. The key component is a point-free notion of propositions. Our construction suggests that strict algebraic structures can be defined along the same lines in intensional type theory.
Cite as
István Donkó and Ambrus Kaposi. Internal Strict Propositions Using Point-Free Equations. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{donko_et_al:LIPIcs.TYPES.2021.6,
author = {Donk\'{o}, Istv\'{a}n and Kaposi, Ambrus},
title = {{Internal Strict Propositions Using Point-Free Equations}},
booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)},
pages = {6:1--6:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-254-9},
ISSN = {1868-8969},
year = {2022},
volume = {239},
editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.6},
URN = {urn:nbn:de:0030-drops-167759},
doi = {10.4230/LIPIcs.TYPES.2021.6},
annote = {Keywords: Martin-L\"{o}f’s type theory, intensional type theory, function extensionality, setoid model, homotopy type theory}
}
Document
Constructive Cut Elimination in Geometric Logic
Abstract
A constructivisation of the cut-elimination proof for sequent calculi for classical and intuitionistic infinitary logic with geometric rules - given in earlier work by the second author - is presented. This is achieved through a procedure in which the non-constructive transfinite induction on the commutative sum of ordinals is replaced by two instances of Brouwer’s Bar Induction. Additionally, a proof of Barr’s Theorem for geometric theories that uses only constructively acceptable proof-theoretical tools is obtained.
Cite as
Giulio Fellin, Sara Negri, and Eugenio Orlandelli. Constructive Cut Elimination in Geometric Logic. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 7:1-7:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{fellin_et_al:LIPIcs.TYPES.2021.7,
author = {Fellin, Giulio and Negri, Sara and Orlandelli, Eugenio},
title = {{Constructive Cut Elimination in Geometric Logic}},
booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)},
pages = {7:1--7:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-254-9},
ISSN = {1868-8969},
year = {2022},
volume = {239},
editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.7},
URN = {urn:nbn:de:0030-drops-167763},
doi = {10.4230/LIPIcs.TYPES.2021.7},
annote = {Keywords: Geometric theories, sequent calculi, axioms-as-rules, infinitary logic, constructive cut elimination}
}
Document
A Succinct Formalization of the Completeness of First-Order Logic
Abstract
I succinctly formalize the soundness and completeness of a small Hilbert system for first-order logic in the proof assistant Isabelle/HOL. The proof combines and details ideas from de Bruijn, Henkin, Herbrand, Hilbert, Hintikka, Lindenbaum, Smullyan and others in a novel way, and I use a declarative style, custom notation and proof automation to obtain a readable formalization. The formalized definitions of Hintikka sets and Herbrand structures allow open and closed formulas to be treated uniformly, making free variables a non-concern. This paper collects important techniques in mathematical logic in a way suited for both study and further work.
Cite as
Asta Halkjær From. A Succinct Formalization of the Completeness of First-Order Logic. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 8:1-8:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{from:LIPIcs.TYPES.2021.8,
author = {From, Asta Halkj{\ae}r},
title = {{A Succinct Formalization of the Completeness of First-Order Logic}},
booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)},
pages = {8:1--8:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-254-9},
ISSN = {1868-8969},
year = {2022},
volume = {239},
editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.8},
URN = {urn:nbn:de:0030-drops-167771},
doi = {10.4230/LIPIcs.TYPES.2021.8},
annote = {Keywords: First-Order Logic, Completeness, Isabelle/HOL}
}
Document
Simulating Large Eliminations in Cedille
Abstract
Large eliminations provide an expressive mechanism for arity- and type-generic programming. However, as large eliminations are closely tied to a type theory’s primitive notion of inductive type, this expressivity is not expected within polymorphic lambda calculi in which datatypes are encoded using impredicative quantification. We report progress on simulating large eliminations for datatype encodings in one such type theory, the calculus of dependent lambda eliminations (CDLE). Specifically, we show that the expected computation rules for large eliminations, expressed using a derived type of extensional equality of types, can be proven within CDLE. We present several case studies, demonstrating the adequacy of this simulation for a variety of generic programming tasks, and a generic formulation of the simulation allowing its use for a broad family of datatype encodings. All results have been mechanically checked by Cedille, an implementation of CDLE.
Cite as
Christa Jenkins, Andrew Marmaduke, and Aaron Stump. Simulating Large Eliminations in Cedille. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 9:1-9:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{jenkins_et_al:LIPIcs.TYPES.2021.9,
author = {Jenkins, Christa and Marmaduke, Andrew and Stump, Aaron},
title = {{Simulating Large Eliminations in Cedille}},
booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)},
pages = {9:1--9:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-254-9},
ISSN = {1868-8969},
year = {2022},
volume = {239},
editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.9},
URN = {urn:nbn:de:0030-drops-167784},
doi = {10.4230/LIPIcs.TYPES.2021.9},
annote = {Keywords: large eliminations, generic programming, impredicative encodings, Cedille, Mendler algebra}
}
Document
Quantitative Polynomial Functors
Abstract
We investigate containers and polynomial functors in Quantitative Type Theory, and give initial algebra semantics of inductive data types in the presence of linearity. We show that reasoning by induction is supported, and equivalent to initiality, also in the linear setting.
Cite as
Georgi Nakov and Fredrik Nordvall Forsberg. Quantitative Polynomial Functors. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{nakov_et_al:LIPIcs.TYPES.2021.10,
author = {Nakov, Georgi and Nordvall Forsberg, Fredrik},
title = {{Quantitative Polynomial Functors}},
booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)},
pages = {10:1--10:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-254-9},
ISSN = {1868-8969},
year = {2022},
volume = {239},
editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.10},
URN = {urn:nbn:de:0030-drops-167795},
doi = {10.4230/LIPIcs.TYPES.2021.10},
annote = {Keywords: quantitative type theory, polynomial functors, inductive data types}
}
Document
Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes
Abstract
Type-preserving translations are effective rigorous tools in the study of core programming calculi. In this paper, we develop a new typed translation that connects sequential and concurrent calculi; it is governed by type systems that control resource consumption. Our main contribution is the source language, a new resource λ-calculus with non-collapsing non-determinism and failures, dubbed uλ^{↯}_{⊕}. In uλ^{↯}_{⊕}, resources are split into linear and unrestricted; failures are explicit and arise from this distinction. We define a type system based on intersection types to control resources and fail-prone computation. The target language is 𝗌π, an existing session-typed π-calculus that results from a Curry-Howard correspondence between linear logic and session types. Our typed translation subsumes our prior work; interestingly, it treats unrestricted resources in uλ^{↯}_{⊕} as client-server session behaviours in 𝗌π.
Cite as
Joseph W. N. Paulus, Daniele Nantes-Sobrinho, and Jorge A. Pérez. Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 11:1-11:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{paulus_et_al:LIPIcs.TYPES.2021.11,
author = {Paulus, Joseph W. N. and Nantes-Sobrinho, Daniele and P\'{e}rez, Jorge A.},
title = {{Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes}},
booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)},
pages = {11:1--11:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-254-9},
ISSN = {1868-8969},
year = {2022},
volume = {239},
editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.11},
URN = {urn:nbn:de:0030-drops-167808},
doi = {10.4230/LIPIcs.TYPES.2021.11},
annote = {Keywords: Resource \lambda-calculus, intersection types, session types, process calculi}
}
Document
Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus
Abstract
So far, several typed lambda-calculus systems were combined with algebraic rewrite rules, and the termination (in other words, strong normalisation) problem of the combined systems was discussed. By the size-based approach, Blanqui formulated a termination criterion for simply typed lambda-calculus with algebraic rewrite rules which guarantees, in some specific cases, the termination of the rewrite relation induced by beta-reduction and algebraic rewrite rules on strictly or non-strictly positive inductive types. Using the inflationary fixed-point construction, we extend this termination criterion so that it is possible to show the termination of the rewrite relation induced by some rewrite rules on types which are called non-positive types. In addition, we note that a condition in Blanqui’s proof can be dropped, and this improves the criterion also for non-strictly positive inductive types.
Cite as
Yuta Takahashi. Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{takahashi:LIPIcs.TYPES.2021.12,
author = {Takahashi, Yuta},
title = {{Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus}},
booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)},
pages = {12:1--12:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-254-9},
ISSN = {1868-8969},
year = {2022},
volume = {239},
editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.12},
URN = {urn:nbn:de:0030-drops-167811},
doi = {10.4230/LIPIcs.TYPES.2021.12},
annote = {Keywords: termination, higher-order rewriting, non-positive types, inductive types}
}