eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-15
69
0
0
10.4230/LIPIcs.TYPES.2015
article
LIPIcs, Volume 69, TYPES'15, Complete Volume
Uustalu, Tarmo
LIPIcs, Volume 69, TYPES'15, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol069-types2015/LIPIcs.TYPES.2015/LIPIcs.TYPES.2015.pdf
Mathematical Logic and Formal Languages: Mathematical Logic - Lambda calculus and related systems
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-15
69
0:i
0:xii
10.4230/LIPIcs.TYPES.2015.0
article
Front Matter, Table of Contents, Preface, External Reviewers
Uustalu, Tarmo
Front Matter, Table of Contents, Preface, External Reviewers
https://drops.dagstuhl.de/storage/00lipics/lipics-vol069-types2015/LIPIcs.TYPES.2015.0/LIPIcs.TYPES.2015.0.pdf
Front Matter
Table of Contents
Preface
External Reviewers
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-15
69
1:1
1:34
10.4230/LIPIcs.TYPES.2015.1
article
A Type Theory for Probabilistic and Bayesian Reasoning
Adams, Robin
Jacobs, Bart
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol069-types2015/LIPIcs.TYPES.2015.1/LIPIcs.TYPES.2015.1.pdf
Probabilistic programming
probabilistic algorithm
type theory
effect module
Bayesian reasoning
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-15
69
2:1
2:23
10.4230/LIPIcs.TYPES.2015.2
article
Heterogeneous Substitution Systems Revisited
Ahrens, Benedikt
Matthes, Ralph
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol069-types2015/LIPIcs.TYPES.2015.2/LIPIcs.TYPES.2015.2.pdf
formalization of category theory
nested datatypes
Mendler-style recursion schemes
representation of substitution in languages with variable binding
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-15
69
3:1
3:27
10.4230/LIPIcs.TYPES.2015.3
article
Towards a Cubical Type Theory without an Interval
Altenkirch, Thorsten
Kaposi, Ambrus
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol069-types2015/LIPIcs.TYPES.2015.3/LIPIcs.TYPES.2015.3.pdf
homotopy type theory
parametricity
univalence
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-15
69
4:1
4:29
10.4230/LIPIcs.TYPES.2015.4
article
Constrained Polymorphic Types for a Calculus with Name Variables
Ancona, Davide
Giannini, Paola
Zucca, Elena
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol069-types2015/LIPIcs.TYPES.2015.4/LIPIcs.TYPES.2015.4.pdf
open code
incremental rebinding
name polymorphism
metaprogramming
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-15
69
5:1
5:34
10.4230/LIPIcs.TYPES.2015.5
article
Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom
Cohen, Cyril
Coquand, Thierry
Huber, Simon
Mörtberg, Anders
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol069-types2015/LIPIcs.TYPES.2015.5/LIPIcs.TYPES.2015.5.pdf
univalence axiom
dependent type theory
cubical sets
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-15
69
6:1
6:23
10.4230/LIPIcs.TYPES.2015.6
article
Efficient Type Checking for Path Polymorphism
Edi, Juan
Viso, Andrés
Bonelli, Eduardo
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol069-types2015/LIPIcs.TYPES.2015.6/LIPIcs.TYPES.2015.6.pdf
lambda-calculus
pattern matching
path polymorphism
type checking
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-15
69
7:1
7:21
10.4230/LIPIcs.TYPES.2015.7
article
A Certified Study of a Reversible Programming Language
Paolini, Luca
Piccolo, Mauro
Roversi, Luca
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol069-types2015/LIPIcs.TYPES.2015.7/LIPIcs.TYPES.2015.7.pdf
reversible computing
Janus
operational semantics
bi-deterministic evaluation
categorical semantics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-15
69
8:1
8:25
10.4230/LIPIcs.TYPES.2015.8
article
Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation
Parmann, Erik
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol069-types2015/LIPIcs.TYPES.2015.8/LIPIcs.TYPES.2015.8.pdf
constructive logic
simplicial sets
semantics of simple types
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-03-15
69
9:1
9:27
10.4230/LIPIcs.TYPES.2015.9
article
Pi-Ware: Hardware Description and Verification in Agda
Pizani Flor, João Paulo
Swierstra, Wouter
Sijsling, Yorick
There is a long tradition of modelling digital circuits using functional programming languages. This paper demonstrates that by employing dependently typed programming languages, it becomes possible to define circuit descriptions that may be simulated, tested, verified and synthesized using a single language. The resulting domain specific embedded language, Pi-Ware, makes it possible to define and verify entire families of circuits at once. We demonstrate this by defining an algebra of parallel prefix circuits, proving their correctness and further algebraic properties.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol069-types2015/LIPIcs.TYPES.2015.9/LIPIcs.TYPES.2015.9.pdf
dependently typed programming
Agda
EDSL
hardware description languages
functional programming