Preface
Pierre-Louis Curien, Patrick Baillot, Luca Paolini |
|
|
| Initial Algebra Semantics for Cyclic Sharing Tree Structures |
|
Makoto Hamana
|
|
|
| Interactive Learning-Based Realizability for Heyting Arithmetic with EM₁ |
|
Federico Aschieri and Stefano Berardi
|
|
|
| Weak omega-categories from intensional type theory |
|
Peter LeFa Lumsdaine
|
|
|
| Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance |
|
William Lovas and Frank Pfenning
|
|
|
| Bounded Linear Logic, Revisited |
|
Ugo Dal Lago and Martin Hofmann
|
|
|
| A Logical Foundation for Environment Classifiers |
|
Takeshi Tsukada and Atsushi Igarashi
|
|
|
| On the meaning of logical completeness |
|
Michele Basaldella and Kazushige Terui
|
|
|
| Semantics of Typed Lambda-Calculus with Constructors |
|
Barbara Petit
|
|
|
| Existential witness extraction in classical realizability and via a negative translation |
|
Alexandre Miquel
|
|
|
| A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance |
|
Andreas Abel, Thierry Coquand and Miguel Pagano
|
|
|
| Realizability algebras: a program to well order R |
|
Jean-Louis Krivine
|
|
|
| On the mathematical synthesis of equational logics |
|
Marcelo Fiore and Chung-Kil Hur
|
|
|
| Realizability algebras II : new models of ZF + DC |
|
Jean-Louis Krivine
|
|
|
| Derivation Lengths Classification of Gödel's T Extending Howard's Assignment |
|
Gunnar Wilken and Andreas Weiermann
|
|
|
Creative Commons