![](https://dblp.dagstuhl.de/img/logo.ua.320x120.png)
![](https://dblp.dagstuhl.de/img/dropdown.dark.16x16.png)
![](https://dblp.dagstuhl.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
![search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
default search action
28th TYPES 2022: Nantes, France
- Delia Kesner
, Pierre-Marie Pédrot:
28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France. LIPIcs 269, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2023, ISBN 978-3-95977-285-3 - Front Matter, Table of Contents, Preface, Conference Organization. 0:1-0:8
- Dominic P. Mulligan:
All Watched Over by Machines of Loving Grace. 1:1-1:23 - Herman Geuvers, Tonny Hurkens:
Classical Natural Deduction from Truth Tables. 2:1-2:27 - Andrea Colledan, Ugo Dal Lago:
On Dynamic Lifting and Effect Typing in Circuit Description Languages. 3:1-3:21 - Émilie Grienenberger:
Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory. 4:1-4:23 - Luca Padovani:
On the Fair Termination of Client-Server Sessions. 5:1-5:21 - Philipp Stassen, Daniel Gratzer, Lars Birkedal:
{mitten}: A Flexible Multimodal Proof Assistant. 6:1-6:23 - Nathan Mull:
An Irrelevancy-Eliminating Translation of Pure Type Systems. 7:1-7:21 - Fábio Reis, Sandra Alves, Mário Florido
:
Linear Rank Intersection Types. 8:1-8:21 - Felix Bradley
, Zhaohui Luo:
A Metatheoretic Analysis of Subtype Universes. 9:1-9:21 - Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tamás Végh:
The Münchhausen Method in Type Theory. 10:1-10:20 - Catherine Dubois, Nicolas Magaud, Alain Giorgetti:
Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families. 11:1-11:19 - Amélie Ledein, Valentin Blot, Catherine Dubois:
A Semantics of 𝕂 into Dedukti. 12:1-12:22 - Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó:
Type Theory with Explicit Universe Polymorphism. 13:1-13:16 - Max Zeuner
, Anders Mörtberg:
A Univalent Formalization of Constructive Affine Schemes. 14:1-14:24 - Kobe Wullaert, Ralph Matthes, Benedikt Ahrens:
Univalent Monoidal Categories. 15:1-15:21
![](https://dblp.dagstuhl.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.