LIPIcs, Volume 97, TYPES 2016

• Silvia Ghilezan, Herman Geuvers, and Jelena Ivetić LIPIcs, Volume 97, TYPES'16, Complete Volume 10.4230/LIPIcs.TYPES.2016
• Silvia Ghilezan, Herman Geuvers, and Jelena Ivetic Front Matter, Table of Contents, Preface, Conference Organization 10.4230/LIPIcs.TYPES.2016.0
• Dale Miller Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper) 10.4230/LIPIcs.TYPES.2016.1
• Simona Ronchi Della Rocca Intersection Types and Denotational Semantics: An Extended Abstract (Invited Paper) 10.4230/LIPIcs.TYPES.2016.2
• Robin Adams, Marc Bezem, and Thierry Coquand A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic 10.4230/LIPIcs.TYPES.2016.3
• Federico Aschieri and Matteo Manighetti On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic 10.4230/LIPIcs.TYPES.2016.4
• Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, and Christopher A. Stone Design and Implementation of the Andromeda Proof Assistant 10.4230/LIPIcs.TYPES.2016.5
• Marc Bezem, Thierry Coquand, Keiko Nakata, and Erik Parmann Realizability at Work: Separating Two Constructive Notions of Finiteness 10.4230/LIPIcs.TYPES.2016.6
• Auke B. Booij, Martín H. Escardó, Peter LeFanu Lumsdaine, and Michael Shulman Parametricity, Automorphisms of the Universe, and Excluded Middle 10.4230/LIPIcs.TYPES.2016.7
• Jacek Chrzaszcz, Aleksy Schubert, and Jakub Zakrzewski Coq Support in HAHA 10.4230/LIPIcs.TYPES.2016.8
• Lukasz Czajka A Shallow Embedding of Pure Type Systems into First-Order Logic 10.4230/LIPIcs.TYPES.2016.9
• José Espírito Santo, Maria João Frade, and Luís Pinto Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts 10.4230/LIPIcs.TYPES.2016.10
• Kuen-Bang Hou (Favonia) and Robert Harper Covering Spaces in Homotopy Type Theory 10.4230/LIPIcs.TYPES.2016.11
• Bashar Igried and Anton Setzer Defining Trace Semantics for CSP-Agda 10.4230/LIPIcs.TYPES.2016.12
• Georgiana Elena Lungu and Zhaohui Luo On Subtyping in Type Theories with Canonical Objects 10.4230/LIPIcs.TYPES.2016.13
• Érik Martin-Dorel and Sergei Soloviev A Formal Study of Boolean Games with Random Formulas as Payoff Functions 10.4230/LIPIcs.TYPES.2016.14
• Richard Statman The Completeness of BCD for an Operational Semantics 10.4230/LIPIcs.TYPES.2016.15