17 Search Results for "Uustalu, Tarmo"


Volume

LIPIcs, Volume 69

21st International Conference on Types for Proofs and Programs (TYPES 2015)

TYPES 2015, May 18-21, 2015, Tallinn, Estonia

Editors: Tarmo Uustalu

Document
Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor

Authors: Niccolò Veltri

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)


Abstract
The finite powerset functor is a construct frequently employed for the specification of nondeterministic transition systems as coalgebras. The final coalgebra of the finite powerset functor, whose elements characterize the dynamical behavior of transition systems, is a well-understood object which enjoys many equivalent presentations in set-theoretic foundations based on classical logic. In this paper, we discuss various constructions of the final coalgebra of the finite powerset functor in constructive type theory, and we formalize our results in the Cubical Agda proof assistant. Using setoids, the final coalgebra of the finite powerset functor can be defined from the final coalgebra of the list functor. Using types instead of setoids, as it is common in homotopy type theory, one can specify the finite powerset datatype as a higher inductive type and define its final coalgebra as a coinductive type. Another construction is obtained by quotienting the final coalgebra of the list functor, but the proof of finality requires the assumption of the axiom of choice. We conclude the paper with an analysis of a classical construction by James Worrell, and show that its adaptation to our constructive setting requires the presence of classical axioms such as countable choice and the lesser limited principle of omniscience.

Cite as

Niccolò Veltri. Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{veltri:LIPIcs.FSCD.2021.22,
  author =	{Veltri, Niccol\`{o}},
  title =	{{Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{22:1--22:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.22},
  URN =		{urn:nbn:de:0030-drops-142601},
  doi =		{10.4230/LIPIcs.FSCD.2021.22},
  annote =	{Keywords: type theory, finite powerset, final coalgebra, Cubical Agda}
}
Document
Decomposing Comonad Morphisms

Authors: Danel Ahman and Tarmo Uustalu

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)


Abstract
The analysis of set comonads whose underlying functor is a container functor in terms of directed containers makes it a simple observation that any morphism between two such comonads factors through a third one by two comonad morphisms, whereof the first is identity on shapes and the second is identity on positions in every shape. This observation turns out to generalize into a much more involved result about comonad morphisms to comonads whose underlying functor preserves Cartesian natural transformations to itself on any category with finite limits. The bijection between comonad coalgebras and comonad morphisms from costate comonads thus also yields a decomposition of comonad coalgebras.

Cite as

Danel Ahman and Tarmo Uustalu. Decomposing Comonad Morphisms. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{ahman_et_al:LIPIcs.CALCO.2019.14,
  author =	{Ahman, Danel and Uustalu, Tarmo},
  title =	{{Decomposing Comonad Morphisms}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{14:1--14:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.14},
  URN =		{urn:nbn:de:0030-drops-114427},
  doi =		{10.4230/LIPIcs.CALCO.2019.14},
  annote =	{Keywords: container functors (polynomial functors), container comonads, comonad morphisms and comonad coalgebras, cofunctors, lenses}
}
Document
Reordering Derivatives of Trace Closures of Regular Languages

Authors: Hendrik Maarand and Tarmo Uustalu

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
We provide syntactic derivative-like operations, defined by recursion on regular expressions, in the styles of both Brzozowski and Antimirov, for trace closures of regular languages. Just as the Brzozowski and Antimirov derivative operations for regular languages, these syntactic reordering derivative operations yield deterministic and nondeterministic automata respectively. But trace closures of regular languages are in general not regular, hence these automata cannot generally be finite. Still, as we show, for star-connected expressions, the Antimirov and Brzozowski automata, suitably quotiented, are finite. We also define a refined version of the Antimirov reordering derivative operation where parts-of-derivatives (states of the automaton) are nonempty lists of regular expressions rather than single regular expressions. We define the uniform scattering rank of a language and show that, for a regexp whose language has finite uniform scattering rank, the truncation of the (generally infinite) refined Antimirov automaton, obtained by removing long states, is finite without any quotienting, but still accepts the trace closure. We also show that star-connected languages have finite uniform scattering rank.

Cite as

Hendrik Maarand and Tarmo Uustalu. Reordering Derivatives of Trace Closures of Regular Languages. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 40:1-40:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{maarand_et_al:LIPIcs.CONCUR.2019.40,
  author =	{Maarand, Hendrik and Uustalu, Tarmo},
  title =	{{Reordering Derivatives of Trace Closures of Regular Languages}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{40:1--40:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.40},
  URN =		{urn:nbn:de:0030-drops-109426},
  doi =		{10.4230/LIPIcs.CONCUR.2019.40},
  annote =	{Keywords: Mazurkiewicz traces, trace closure, regular languages, finite automata, language derivatives, scattering rank, star-connected expressions}
}
Document
Modal Embeddings and Calling Paradigms

Authors: José Espírito Santo, Luís Pinto, and Tarmo Uustalu

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)


Abstract
We study the computational interpretation of the two standard modal embeddings, usually named after Girard and Gödel, of intuitionistic logic into IS4. As source system we take either the call-by-name (cbn) or the call-by-value (cbv) lambda-calculus with simple types. The target system can be taken to be the, arguably, simplest fragment of IS4, here recast as a very simple lambda-calculus equipped with an indeterminate lax monoidal comonad. A slight refinement of the target and of the embeddings shows that: the target is a calculus indifferent to the calling paradigms cbn/cbv, obeying a new paradigm that we baptize call-by-box (cbb), and enjoying standardization; and that Girard’s (resp. Gödel’s) embbedding is a translation of cbn (resp. cbv) lambda-calculus into this calculus, using a compilation technique we call protecting-by-a-box, enjoying the preservation and reflection properties known for cps translations - but in a stronger form that allows the extraction of standardization for cbn or cbv as consequence of standardization for cbb. The modal target and embeddings achieve thus an unification of call-by-name and call-by-value as call-by-box.

Cite as

José Espírito Santo, Luís Pinto, and Tarmo Uustalu. Modal Embeddings and Calling Paradigms. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{espiritosanto_et_al:LIPIcs.FSCD.2019.18,
  author =	{Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s and Uustalu, Tarmo},
  title =	{{Modal Embeddings and Calling Paradigms}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{18:1--18:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.18},
  URN =		{urn:nbn:de:0030-drops-105256},
  doi =		{10.4230/LIPIcs.FSCD.2019.18},
  annote =	{Keywords: intuitionistic S4, call-by-name, call-by-value, comonadic lambda-calculus, standardization, indifference property}
}
Document
Complete Volume
LIPIcs, Volume 69, TYPES'15, Complete Volume

Authors: Tarmo Uustalu

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)


Abstract
LIPIcs, Volume 69, TYPES'15, Complete Volume

Cite as

21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@Proceedings{uustalu:LIPIcs.TYPES.2015,
  title =	{{LIPIcs, Volume 69, TYPES'15, Complete Volume}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015},
  URN =		{urn:nbn:de:0030-drops-86220},
  doi =		{10.4230/LIPIcs.TYPES.2015},
  annote =	{Keywords: Mathematical Logic and Formal Languages: Mathematical Logic - Lambda calculus and related systems}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, External Reviewers

Authors: Tarmo Uustalu

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)


Abstract
Front Matter, Table of Contents, Preface, External Reviewers

Cite as

21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{uustalu:LIPIcs.TYPES.2015.0,
  author =	{Uustalu, Tarmo},
  title =	{{Front Matter, Table of Contents, Preface, External Reviewers}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{0:i--0:xii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.0},
  URN =		{urn:nbn:de:0030-drops-84704},
  doi =		{10.4230/LIPIcs.TYPES.2015.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, External Reviewers}
}
Document
A Type Theory for Probabilistic and Bayesian Reasoning

Authors: Robin Adams and Bart Jacobs

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)


Abstract
This paper introduces a novel type theory and logic for probabilistic reasoning. Its logic is quantitative, with fuzzy predicates. It includes normalisation and conditioning of states. This conditioning uses a key aspect that distinguishes our probabilistic type theory from quantum type theory, namely the bijective correspondence between predicates and side-effect free actions (called instrument, or assert, maps). The paper shows how suitable computation rules can be derived from this predicate-action correspondence, and uses these rules for calculating conditional probabilities in two well-known examples of Bayesian reasoning in (graphical) models. Our type theory may thus form the basis for a mechanisation of Bayesian inference.

Cite as

Robin Adams and Bart Jacobs. A Type Theory for Probabilistic and Bayesian Reasoning. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 1:1-1:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{adams_et_al:LIPIcs.TYPES.2015.1,
  author =	{Adams, Robin and Jacobs, Bart},
  title =	{{A Type Theory for Probabilistic and Bayesian Reasoning}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{1:1--1:34},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.1},
  URN =		{urn:nbn:de:0030-drops-84714},
  doi =		{10.4230/LIPIcs.TYPES.2015.1},
  annote =	{Keywords: Probabilistic programming, probabilistic algorithm, type theory, effect module, Bayesian reasoning}
}
Document
Heterogeneous Substitution Systems Revisited

Authors: Benedikt Ahrens and Ralph Matthes

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)


Abstract
Matthes and Uustalu (TCS 327(1--2):155--174, 2004) presented a categorical description of substitution systems capable of capturing syntax involving binding which is independent of whether the syntax is made up from least or greatest fixed points. We extend this work in two directions: we continue the analysis by creating more categorical structure, in particular by organizing substitution systems into a category and studying its properties, and we develop the proofs of the results of the cited paper and our new ones in UniMath, a recent library of univalent mathematics formalized in the Coq theorem prover.

Cite as

Benedikt Ahrens and Ralph Matthes. Heterogeneous Substitution Systems Revisited. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 2:1-2:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{ahrens_et_al:LIPIcs.TYPES.2015.2,
  author =	{Ahrens, Benedikt and Matthes, Ralph},
  title =	{{Heterogeneous Substitution Systems Revisited}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{2:1--2:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.2},
  URN =		{urn:nbn:de:0030-drops-84724},
  doi =		{10.4230/LIPIcs.TYPES.2015.2},
  annote =	{Keywords: formalization of category theory, nested datatypes, Mendler-style recursion schemes, representation of substitution in languages with variable binding}
}
Document
Towards a Cubical Type Theory without an Interval

Authors: Thorsten Altenkirch and Ambrus Kaposi

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)


Abstract
Following the cubical set model of type theory which validates the univalence axiom, cubical type theories have been developed that interpret the identity type using an interval pretype. These theories start from a geometric view of equality. A proof of equality is encoded as a term in a context extended by the interval pretype. Our goal is to develop a cubical theory where the identity type is defined recursively over the type structure, and the geometry arises from these definitions. In this theory, cubes are present explicitly, e.g., a line is a telescope with 3 elements: two endpoints and the connecting equality. This is in line with Bernardy and Moulin's earlier work on internal parametricity. In this paper we present a naive syntax for internal parametricity and by replacing the parametric interpretation of the universe, we extend it to univalence. However, we do not know how to compute in this theory. As a second step, we present a version of the theory for parametricity with named dimensions which has an operational semantics. Extending this syntax to univalence is left as further work.

Cite as

Thorsten Altenkirch and Ambrus Kaposi. Towards a Cubical Type Theory without an Interval. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 3:1-3:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{altenkirch_et_al:LIPIcs.TYPES.2015.3,
  author =	{Altenkirch, Thorsten and Kaposi, Ambrus},
  title =	{{Towards a Cubical Type Theory without an Interval}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{3:1--3:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.3},
  URN =		{urn:nbn:de:0030-drops-84739},
  doi =		{10.4230/LIPIcs.TYPES.2015.3},
  annote =	{Keywords: homotopy type theory, parametricity, univalence}
}
Document
Constrained Polymorphic Types for a Calculus with Name Variables

Authors: Davide Ancona, Paola Giannini, and Elena Zucca

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)


Abstract
We extend the simply-typed lambda-calculus with a mechanism for dynamic rebinding of code based on parametric nominal interfaces. That is, we introduce values which represent single fragments, or families of named fragments, of open code, where free variables are associated with names which do not obey \alpha-equivalence. In this way, code fragments can be passed as function arguments and manipulated, through their nominal interface, by operators such as rebinding, overriding and renaming. Moreover, by using name variables, it is possible to write terms which are parametric in their nominal interface and/or in the way it is adapted, greatly enhancing expressivity. However, in order to prevent conflicts when instantiating name variables, the name-polymorphic types of such terms need to be equipped with simple {inequality} constraints. We show soundness of the type system.

Cite as

Davide Ancona, Paola Giannini, and Elena Zucca. Constrained Polymorphic Types for a Calculus with Name Variables. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 4:1-4:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{ancona_et_al:LIPIcs.TYPES.2015.4,
  author =	{Ancona, Davide and Giannini, Paola and Zucca, Elena},
  title =	{{Constrained Polymorphic Types for a Calculus with Name Variables}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{4:1--4:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.4},
  URN =		{urn:nbn:de:0030-drops-84744},
  doi =		{10.4230/LIPIcs.TYPES.2015.4},
  annote =	{Keywords: open code, incremental rebinding, name polymorphism, metaprogramming}
}
Document
Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom

Authors: Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)


Abstract
This paper presents a type theory in which it is possible to directly manipulate $n$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.

Cite as

Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 5:1-5:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{cohen_et_al:LIPIcs.TYPES.2015.5,
  author =	{Cohen, Cyril and Coquand, Thierry and Huber, Simon and M\"{o}rtberg, Anders},
  title =	{{Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{5:1--5:34},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.5},
  URN =		{urn:nbn:de:0030-drops-84754},
  doi =		{10.4230/LIPIcs.TYPES.2015.5},
  annote =	{Keywords: univalence axiom, dependent type theory, cubical sets}
}
Document
Efficient Type Checking for Path Polymorphism

Authors: Juan Edi, Andrés Viso, and Eduardo Bonelli

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)


Abstract
A type system combining type application, constants as types, union types (associative, commutative and idempotent) and recursive types has recently been proposed for statically typing path polymorphism, the ability to define functions that can operate uniformly over recursively specified applicative data structures. A typical pattern such functions resort to is \dataterm{x}{y} which decomposes a compound, in other words any applicative tree structure, into its parts. We study type-checking for this type system in two stages. First we propose algorithms for checking type equivalence and subtyping based on coinductive characterizations of those relations. We then formulate a syntax-directed presentation and prove its equivalence with the original one. This yields a type-checking algorithm which unfortunately has exponential time complexity in the worst case. A second algorithm is then proposed, based on automata techniques, which yields a polynomial-time type-checking algorithm.

Cite as

Juan Edi, Andrés Viso, and Eduardo Bonelli. Efficient Type Checking for Path Polymorphism. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{edi_et_al:LIPIcs.TYPES.2015.6,
  author =	{Edi, Juan and Viso, Andr\'{e}s and Bonelli, Eduardo},
  title =	{{Efficient Type Checking for Path Polymorphism}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{6:1--6:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.6},
  URN =		{urn:nbn:de:0030-drops-84761},
  doi =		{10.4230/LIPIcs.TYPES.2015.6},
  annote =	{Keywords: lambda-calculus, pattern matching, path polymorphism, type checking}
}
Document
A Certified Study of a Reversible Programming Language

Authors: Luca Paolini, Mauro Piccolo, and Luca Roversi

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)


Abstract
We advance in the study of the semantics of Janus, a C-like reversible programming language. Our study makes utterly explicit some backward and forward evaluation symmetries. We want to deepen mathematical knowledge about the foundations and design principles of reversible computing and programming languages. We formalize a big-step operational semantics and a denotational semantics of Janus. We show a full abstraction result between the operational and denotational semantics. Last, we certify our results by means of the proof assistant Matita.

Cite as

Luca Paolini, Mauro Piccolo, and Luca Roversi. A Certified Study of a Reversible Programming Language. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 7:1-7:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{paolini_et_al:LIPIcs.TYPES.2015.7,
  author =	{Paolini, Luca and Piccolo, Mauro and Roversi, Luca},
  title =	{{A Certified Study of a Reversible Programming Language}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{7:1--7:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.7},
  URN =		{urn:nbn:de:0030-drops-84771},
  doi =		{10.4230/LIPIcs.TYPES.2015.7},
  annote =	{Keywords: reversible computing, Janus, operational semantics, bi-deterministic evaluation, categorical semantics}
}
Document
Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation

Authors: Erik Parmann

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)


Abstract
Functional Kan simplicial sets are simplicial sets in which the horn-fillers required by the Kan extension condition are given explicitly by functions. We show the non-constructivity of the following basic result: if B and A are functional Kan simplicial sets, then A^B is a Kan simplicial set. This strengthens a similar result for the case of non-functional Kan simplicial sets shown by Bezem, Coquand and Parmann [TLCA 2015, v. 38 of LIPIcs]. Our result shows that-from a constructive point of view-functional Kan simplicial sets are, as it stands, unsatisfactory as a model of even simply typed lambda calculus. Our proof is based on a rather involved Kripke countermodel which has been encoded and verified in the Coq proof assistant.

Cite as

Erik Parmann. Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 8:1-8:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{parmann:LIPIcs.TYPES.2015.8,
  author =	{Parmann, Erik},
  title =	{{Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{8:1--8:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.8},
  URN =		{urn:nbn:de:0030-drops-84787},
  doi =		{10.4230/LIPIcs.TYPES.2015.8},
  annote =	{Keywords: constructive logic, simplicial sets, semantics of simple types}
}
  • Refine by Author
  • 6 Uustalu, Tarmo
  • 2 Ahman, Danel
  • 1 Adams, Robin
  • 1 Ahrens, Benedikt
  • 1 Altenkirch, Thorsten
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Logic
  • 1 Theory of computation → Categorical semantics
  • 1 Theory of computation → Concurrency
  • 1 Theory of computation → Constructive mathematics
  • 1 Theory of computation → Program semantics
  • Show More...

  • Refine by Keyword
  • 2 type theory
  • 1 Agda
  • 1 Bayesian reasoning
  • 1 Cubical Agda
  • 1 EDSL
  • Show More...

  • Refine by Type
  • 16 document
  • 1 volume

  • Refine by Publication Year
  • 12 2018
  • 3 2019
  • 1 2014
  • 1 2021

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