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

Tallinn, Estonia, 18-21 May 2015

Abstracts

Tarmo Uustalu (Ed.)

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)

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

Tallinn, Estonia, 18-21 May 2015

Abstracts

Tarmo Uustalu (Ed.)

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