


default search action
TYPES 2016: Novi Sad, Serbia
- Silvia Ghilezan, Herman Geuvers, Jelena Ivetic:
22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia. LIPIcs 97, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2018, ISBN 978-3-95977-065-1 - Front Matter, Table of Contents, Preface, Conference Organization. 0:i-0:x
- Dale Miller
:
Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper). 1:1-1:16 - Simona Ronchi Della Rocca:
Intersection Types and Denotational Semantics: An Extended Abstract (Invited Paper). 2:1-2:7 - Robin Adams
, Marc Bezem, Thierry Coquand:
A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic. 3:1-3:20 - Federico Aschieri, Matteo Manighetti:
On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic. 4:1-4:17 - Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter
, Matija Pretnar
, Christopher A. Stone
:
Design and Implementation of the Andromeda Proof Assistant. 5:1-5:31 - Marc Bezem, Thierry Coquand, Keiko Nakata, Erik Parmann:
Realizability at Work: Separating Two Constructive Notions of Finiteness. 6:1-6:23 - Auke Bart Booij
, Martín Hötzel Escardó, Peter LeFanu Lumsdaine, Michael Shulman:
Parametricity, Automorphisms of the Universe, and Excluded Middle. 7:1-7:14 - Jacek Chrzaszcz, Aleksy Schubert
, Jakub Zakrzewski:
Coq Support in HAHA. 8:1-8:26 - Lukasz Czajka:
A Shallow Embedding of Pure Type Systems into First-Order Logic. 9:1-9:39 - José Espírito Santo
, Maria João Frade
, Luís Pinto
:
Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts. 10:1-10:27 - Kuen-Bang Hou (Favonia), Robert Harper:
Covering Spaces in Homotopy Type Theory. 11:1-11:16 - Bashar Igried
, Anton Setzer:
Defining Trace Semantics for CSP-Agda. 12:1-12:23 - Georgiana E. Lungu, Zhaohui Luo:
On Subtyping in Type Theories with Canonical Objects. 13:1-13:31 - Érik Martin-Dorel, Sergei Soloviev:
A Formal Study of Boolean Games with Random Formulas as Payoff Functions. 14:1-14:22 - Richard Statman:
The Completeness of BCD for an Operational Semantics. 15:1-15:5

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.