20 Search Results for "Cockx, Jesper"

Volume

LIPIcs, Volume 239

27th International Conference on Types for Proofs and Programs (TYPES 2021)

TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)

Editors: Henning Basold, Jesper Cockx, and Silvia Ghilezan

Document
DOI: 10.4230/OASIcs.FMBC.2024.2
Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda

Authors: Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, and Ulf Norell

Published in: OASIcs, Volume 118, 5th International Workshop on Formal Methods for Blockchains (FMBC 2024)

Abstract
Blockchain systems comprise critical software that handle substantial monetary funds, rendering them excellent candidates for formal verification. One of their core components is the underlying ledger that does all the accounting: keeping track of transactions and their validity, etc. Unfortunately, previous theoretical studies are typically confined to an idealized setting, while specifications for real implementations are scarce; either the functionality is directly implemented without a proper specification, or at best an informal specification is written on paper. The present work expands beyond prior meta-theoretical investigations of the EUTxO model to encompass the full scale of the Cardano blockchain: our formal specification describes a hierarchy of modular transitions that covers all the intricacies of a realistic blockchain, such as fully expressive smart contracts and decentralized governance. It is mechanized in a proof assistant, thus enjoys a higher standard of rigor: type-checking prevents minor oversights that were frequent in previous informal approaches; key meta-theoretical properties can now be formally proven; it is an executable specification against which the implementation in production is being tested for conformance; and it provides firm foundations for smart contract verification. Apart from a safety net to keep us in check, the formalization also provides a guideline for the ledger design: one informs the other in a symbiotic way, especially in the case of state-of-the-art features like decentralized governance, which is an emerging sub-field of blockchain research that however mandates a more exploratory approach. All the results presented in this paper have been mechanized in the Agda proof assistant and are publicly available. In fact, this document is itself a literate Agda script and all rendered code has been successfully type-checked.
Cite as

Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, and Ulf Norell. Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 2:1-2:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{knispel_et_al:OASIcs.FMBC.2024.2,
  author =	{Knispel, Andre and Melkonian, Orestis and Chapman, James and Hill, Alasdair and J\"{a}\"{a}ger, Joosep and DeMeo, William and Norell, Ulf},
  title =	{{Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{2:1--2:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-317-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{118},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2024.2},
  URN =		{urn:nbn:de:0030-drops-198673},
  doi =		{10.4230/OASIcs.FMBC.2024.2},
  annote =	{Keywords: blockchain, distributed ledgers, UTxO, Cardano, formal verification, Agda}
}
Document
DOI: 10.4230/OASIcs.EVCS.2023.6
Dependently Typed Languages in Statix

Authors: Jonathan Brouwer, Jesper Cockx, and Aron Zwaan

Published in: OASIcs, Volume 109, Eelco Visser Commemorative Symposium (EVCS 2023)

Abstract
Static type systems can greatly enhance the quality of programs, but implementing a type checker that is both expressive and user-friendly is challenging and error-prone. The Statix meta-language (part of the Spoofax language workbench) aims to make this task easier by automatically deriving a type checker from a declarative specification of a type system. However, so far Statix has not been used to implement dependent types, which is a class of type systems which require evaluation of terms during type checking. In this paper, we present an implementation of a simple dependently typed language in Statix, and discuss how to extend it with several common features such as inductive data types, universes, and inference of implicit arguments. While we encountered some challenges in the implementation, our conclusion is that Statix is already usable as a tool for implementing dependent types.
Cite as

Jonathan Brouwer, Jesper Cockx, and Aron Zwaan. Dependently Typed Languages in Statix. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 6:1-6:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{brouwer_et_al:OASIcs.EVCS.2023.6,
  author =	{Brouwer, Jonathan and Cockx, Jesper and Zwaan, Aron},
  title =	{{Dependently Typed Languages in Statix}},
  booktitle =	{Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages =	{6:1--6:8},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-267-9},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{109},
  editor =	{L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.EVCS.2023.6},
  URN =		{urn:nbn:de:0030-drops-177769},
  doi =		{10.4230/OASIcs.EVCS.2023.6},
  annote =	{Keywords: Spoofax, Statix, Dependent Types, Scope Graphs, Calculus of Constructions}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.19
Translating Proofs from an Impredicative Type System to a Predicative One

Authors: Thiago Felicissimo, Frédéric Blanqui, and Ashish Kumar Barnawal

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the challenges in this domain is to translate proofs written in proof assistants based on impredicative logics, such as Coq, Matita and the HOL family, to proof assistants based on predicative logics like Agda, whenever impredicativity is not used in an essential way. In this paper we present an algorithm to do such a translation between a core impredicative type system and a core predicative one allowing prenex universe polymorphism like in Agda. It consists in trying to turn a potentially impredicative term into a universe polymorphic term as general as possible. The use of universe polymorphism is justified by the fact that mapping an impredicative universe to a fixed predicative one is not sufficient in most cases. During the algorithm, we need to solve unification problems modulo the max-successor algebra on universe levels. But, in this algebra, there are solvable problems having no most general solution. We however provide an incomplete algorithm whose solutions, when it succeeds, are most general ones. The proposed translation is of course partial, but in practice allows one to translate many proofs that do not use impredicativity in an essential way. Indeed, it was implemented in the tool Predicativize and then used to translate semi-automatically many non-trivial developments from Matita’s arithmetic library to Agda, including Bertrand’s Postulate and Fermat’s Little Theorem, which were not available in Agda yet.
Cite as

Thiago Felicissimo, Frédéric Blanqui, and Ashish Kumar Barnawal. Translating Proofs from an Impredicative Type System to a Predicative One. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{felicissimo_et_al:LIPIcs.CSL.2023.19,
  author =	{Felicissimo, Thiago and Blanqui, Fr\'{e}d\'{e}ric and Barnawal, Ashish Kumar},
  title =	{{Translating Proofs from an Impredicative Type System to a Predicative One}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{19:1--19:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.19},
  URN =		{urn:nbn:de:0030-drops-174801},
  doi =		{10.4230/LIPIcs.CSL.2023.19},
  annote =	{Keywords: Type Theory, Impredicativity, Predicativity, Proof Translation, Universe Polymorphism, Unification Modulo Max, Agda, Dedukti}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.TYPES.2021
LIPIcs, Volume 239, TYPES 2021, Complete Volume

Authors: Henning Basold, Jesper Cockx, and Silvia Ghilezan

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

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
DOI: 10.4230/LIPIcs.TYPES.2021.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Henning Basold, Jesper Cockx, and Silvia Ghilezan

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

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
DOI: 10.4230/LIPIcs.TYPES.2021.1
Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control

Authors: Fahad F. Alhabardi, Arnold Beckmann, Bogdan Lazar, and Anton Setzer

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

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
DOI: 10.4230/LIPIcs.TYPES.2021.2
Formalisation of Dependent Type Theory: The Example of CaTT

Authors: Thibaut Benjamin

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

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
DOI: 10.4230/LIPIcs.TYPES.2021.3
Strictification of Weakly Stable Type-Theoretic Structures Using Generic Contexts

Authors: Rafaël Bocquet

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

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
DOI: 10.4230/LIPIcs.TYPES.2021.4
A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-Löf Type Theory

Authors: William DeMeo and Jacques Carette

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

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
DOI: 10.4230/LIPIcs.TYPES.2021.5
Principal Types as Lambda Nets

Authors: Pietro Di Gianantonio and Marina Lenisa

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

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
DOI: 10.4230/LIPIcs.TYPES.2021.6
Internal Strict Propositions Using Point-Free Equations

Authors: István Donkó and Ambrus Kaposi

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

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
DOI: 10.4230/LIPIcs.TYPES.2021.7
Constructive Cut Elimination in Geometric Logic

Authors: Giulio Fellin, Sara Negri, and Eugenio Orlandelli

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

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
DOI: 10.4230/LIPIcs.TYPES.2021.8
A Succinct Formalization of the Completeness of First-Order Logic

Authors: Asta Halkjær From

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

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
DOI: 10.4230/LIPIcs.TYPES.2021.9
Simulating Large Eliminations in Cedille

Authors: Christa Jenkins, Andrew Marmaduke, and Aaron Stump

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

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}
}
  • Refine by Author
  • 4 Cockx, Jesper
  • 2 Basold, Henning
  • 2 DeMeo, William
  • 2 Ghilezan, Silvia
  • 1 Alhabardi, Fahad F.
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 6 Agda
  • 2 Universe Polymorphism
  • 2 formal verification
  • 2 homotopy type theory
  • 1 Access control
  • Show More...

  • Refine by Type
  • 19 document
  • 1 volume

  • Refine by Publication Year
  • 15 2022
  • 2 2020
  • 2 2023
  • 1 2024

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact