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 |