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

Tallinn, Estonia, 18-21 May 2015

Abstracts

Tarmo Uustalu (Ed.)

Cover
Complete volume in a single file


Title pages, preface and table of contents i
Computer-aided cryptography
Gilles Barthe
1
The troublesome reflection rule
Andrej Bauer
2
Types for quantum computing
Peter Selinger
3
Polynomial functors: a general framework for induction and substitution
Joachim Kock
4
Higher inductive types: what we understand, what we don't
Peter Lefanu Lumsdaine
5
The next 700 modal type assignment systems
Andreas Abel
6
State and effect logics for deterministic, non-deterministic, probabilistic and quantum computation
Robin Adams and Bart Jacobs
8
Refinement types for algebraic effects
Danel Ahman and Gordon Plotkin
10
Non-wellfounded trees in homotopy type theory
Benedikt Ahrens, Paolo Capriotti and Régis Spadotti
12
Substitution systems revisited
Benedikt Ahrens and Ralph Matthes
14
Towards a theory of higher inductive types
Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra and Fredrik Nordvall Forsberg
16
Infinite structures in type theory: problems and approaches
Thorsten Altenkirch, Paolo Capriotti and Nicolai Kraus
18
A nominal syntax for internal parametricity
Thorsten Altenkirch and Ambrus Kaposi
21
Dependent inductive and coinductive types through dialgebras in fibrations
Henning Basold and Herman Geuvers
23
Dialgebra-inspired syntax for dependent inductive and coinductive types
Henning Basold and Herman Geuvers
25
The decision problem for linear tree constraints
Sabine Bauer and Martin Hofmann
27
A presheaf model of parametric type theory
Jean-Philippe Bernardy, Thierry Coquand and Guilhem Moulin
29
Guarded dependent type theory with coinductive types
Aleš Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus Ejlers Møgelberg and Lars Birkedal
31
Rewrite semantics for guarded recursion with universal quantification over clocks
Aleš Bizjak and Rasmus Ejlers Møgelberg
34
Typed realizability for first-order classical analysis
Valentin Blot
36
Quotienting the delay monad by weak bisimilarity
James Chapman, Tarmo Uustalu and Niccolò Veltri
38
A Coq formalization of a sign determination algorithm in real algebraic geometry
Cyril Cohen and Mathieu Kohli
40
A formalized checker for size-optimal sorting networks
Luís Cruz-Filipe and Peter Schneider-Kamp
42
A typed lambda-calculus with call-by-name and call-by-value iteration
Herman Geuvers
44
Two-dimensional proof-relevant parametricity
Neil Ghani, Fredrik Nordvall Forsberg and Federico Orsanigo
46
Intersection types fit well with resource control
Silvia Ghilezan, Jelena Ivetic, Pierre Lescanne and Silvia Likavec
48
Colored intersection types: a semantic approach to higher-order model-checking
Charles Grellois and Paul-André Melliès
50
Implementing dependent types using sequent calculi
Daniel Gustafsson and Nicolas Guenot
53
A proof with side effects of Gödel's completeness theorem suitable for semantic normalisation
Hugo Herbelin
55
A Lambek calculus with dependent types
Zhaohui Luo
57
Introducing a type-theoretical approach to universal grammar
Erkki Luuk
61
The encode-decode method, relationally
James McKinna and Fredrik Nordvall Forsberg
63
Toward dependent choice: a classical sequent calculus with dependent types
Étienne Miquey and Hugo Herbelin
65
Π-Ware: an embedded hardware description language using dependent types
João Paulo Pizani Flor and Wouter Swierstra
67
Well-founded sized types in the calculus of (co)inductive constructions
Jorge Luis Sacchini
69
On relating indexed W-types with ordinary ones
Christian Sattler
71
Axiomatic set theory in type theory
Gert Smolka
73
Cubical sets as a classifying topos
Bas Spitters
75
Total (co)programming with guarded recursion
Andrea Vezzosi
77
Balanced polymorphism and linear lambda calculus
Noam Zeilberger
79
Author index 82

This book of abstracts was produced by the Institute of Cybernetics at Tallinn University of Technology.

ISBN 978-9949-430-86-4 (print)
ISBN 978-9949-430-87-1 (pdf)