Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Delia Kesner, Pierre-Marie Pédrot (eds.) |
28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-285-3 The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
1 | Luca Padovani |
On the Fair Termination of Client-Server Sessions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, pp. 5:1-5:21, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-285-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Philipp Stassen, Daniel Gratzer, Lars Birkedal |
{mitten}: A Flexible Multimodal Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, pp. 6:1-6:23, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-285-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Catherine Dubois, Nicolas Magaud, Alain Giorgetti |
Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, pp. 11:1-11:19, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-285-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Andrea Colledan, Ugo Dal Lago |
On Dynamic Lifting and Effect Typing in Circuit Description Languages. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, pp. 3:1-3:21, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-285-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Max Zeuner, Anders Mörtberg |
A Univalent Formalization of Constructive Affine Schemes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, pp. 14:1-14:24, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-285-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Fábio Reis, Sandra Alves, Mário Florido |
Linear Rank Intersection Types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, pp. 8:1-8:21, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-285-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó |
Type Theory with Explicit Universe Polymorphism. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, pp. 13:1-13:16, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-285-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Amélie Ledein, Valentin Blot, Catherine Dubois |
A Semantics of ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, pp. 12:1-12:22, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-285-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Herman Geuvers, Tonny Hurkens |
Classical Natural Deduction from Truth Tables. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, pp. 2:1-2:27, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-285-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Dominic P. Mulligan |
All Watched Over by Machines of Loving Grace. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, pp. 1:1-1:23, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-285-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Émilie Grienenberger |
Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, pp. 4:1-4:23, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-285-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tamás Végh |
The Münchhausen Method in Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, pp. 10:1-10:20, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-285-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Henning Basold, Jesper Cockx, Silvia Ghilezan (eds.) |
27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference). ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-254-9 The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP BibTeX RDF |
|
1 | Nathan Mull |
An Irrelevancy-Eliminating Translation of Pure Type Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, pp. 7:1-7:21, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-285-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Felix Bradley, Zhaohui Luo |
A Metatheoretic Analysis of Subtype Universes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, pp. 9:1-9:21, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-285-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Kobe Wullaert, Ralph Matthes, Benedikt Ahrens |
Univalent Monoidal Categories. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, pp. 15:1-15:21, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-285-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | |
Front Matter, Table of Contents, Preface, Conference Organization. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, pp. 0:1-0:8, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-285-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Giulio Fellin, Sara Negri, Eugenio Orlandelli |
Constructive Cut Elimination in Geometric Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)., pp. 7:1-7:16, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-254-9. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Yuta Takahashi |
Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)., pp. 12:1-12:23, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-254-9. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Georgi Nakov, Fredrik Nordvall Forsberg |
Quantitative Polynomial Functors. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)., pp. 10:1-10:22, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-254-9. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Thibaut Benjamin |
Formalisation of Dependent Type Theory: The Example of CaTT. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)., pp. 2:1-2:21, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-254-9. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | |
Front Matter, Table of Contents, Preface, Conference Organization. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)., pp. 0:1-0:8, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-254-9. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Fahad F. Alhabardi, Arnold Beckmann, Bogdan Lazar, Anton Setzer |
Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)., pp. 1:1-1:25, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-254-9. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Ugo de'Liguoro, Stefano Berardi, Thorsten Altenkirch (eds.) |
26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-182-5 The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
1 | Pietro Di Gianantonio, Marina Lenisa |
Principal Types as Lambda Nets. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)., pp. 5:1-5:23, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-254-9. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Joseph W. N. Paulus, Daniele Nantes-Sobrinho, Jorge A. Pérez 0001 |
Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)., pp. 11:1-11:24, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-254-9. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Asta Halkjær From |
A Succinct Formalization of the Completeness of First-Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)., pp. 8:1-8:24, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-254-9. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Christa Jenkins, Andrew Marmaduke, Aaron Stump |
Simulating Large Eliminations in Cedille. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)., pp. 9:1-9:22, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-254-9. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | István Donkó, Ambrus Kaposi |
Internal Strict Propositions Using Point-Free Equations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)., pp. 6:1-6:21, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-254-9. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Rafaël Bocquet |
Strictification of Weakly Stable Type-Theoretic Structures Using Generic Contexts. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)., pp. 3:1-3:23, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-254-9. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | William J. DeMeo, Jacques Carette |
A Machine-Checked Proof of Birkhoff's Variety Theorem in Martin-Löf Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)., pp. 4:1-4:21, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-254-9. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Andreas Abel 0001 |
On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy., pp. 1:1-1:21, 2020, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-182-5. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Matteo Manighetti, Dale Miller 0001, Alberto Momigliano |
Two Applications of Logic Programming to Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy., pp. 10:1-10:19, 2020, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-182-5. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Furio Honsell, Marina Lenisa, Ivan Scagnetto |
Λ-Symsym: An Interactive Tool for Playing with Involutions and Types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy., pp. 7:1-7:18, 2020, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-182-5. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Reynald Affeldt, David Nowak |
Extending Equational Monadic Reasoning with Monad Transformers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy., pp. 2:1-2:21, 2020, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-182-5. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Marc Bezem, Assia Mahboubi (eds.) |
25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-158-0 The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
1 | |
Front Matter, Table of Contents, Preface, Conference Organization. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy., pp. 0:1-0:8, 2020, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-182-5. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Pawel Urzyczyn |
Duality in Intuitionistic Propositional Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy., pp. 11:1-11:10, 2020, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-182-5. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Harry Maclean, Zhaohui Luo |
Subtype Universes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy., pp. 9:1-9:16, 2020, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-182-5. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | José Espírito Santo, Ralph Matthes, Luís Pinto 0001 |
Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy., pp. 4:1-4:24, 2020, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-182-5. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Jasper Hugunin |
Why Not W? ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy., pp. 8:1-8:9, 2020, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-182-5. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Gabriel Hondet, Frédéric Blanqui |
Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy., pp. 6:1-6:18, 2020, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-182-5. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Asta Halkjær From |
Synthetic Completeness for a Terminating Seligman-Style Tableau System. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy., pp. 5:1-5:17, 2020, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-182-5. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Guido De Luca, Carlos Luna 0001 |
Towards a Certified Reference Monitor of the Android 10 Permission System. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy., pp. 3:1-3:18, 2020, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-182-5. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, Stephanie Weirich |
Eta-Equivalence in Core Dependent Haskell. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway., pp. 7:1-7:31, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-158-0. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Nils Anders Danielsson |
Higher Inductive Type Eliminators Without Paths. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway., pp. 10:1-10:18, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-158-0. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | |
Front Matter, Table of Contents, Preface, Conference Organization. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway., pp. 0:1-0:10, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-158-0. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Stefano Piceghello |
Coherence for Monoidal Groupoids in HoTT. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway., pp. 8:1-8:20, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-158-0. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Gun Pinyo, Nicolai Kraus |
From Cubes to Twisted Cubes via Graph Morphisms in Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway., pp. 5:1-5:18, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-158-0. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Peter Dybjer, José Espírito Santo, Luís Pinto 0001 (eds.) |
24th International Conference on Types for Proofs and Programs, TYPES 2018, June 18-21, 2018, Braga, Portugal. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-106-1 The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
1 | Stefan Monnier, Nathaniel Bos |
Is Impredicativity Implicitly Implicit? ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway., pp. 9:1-9:19, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-158-0. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Michael Kohlhase, Florian Rabe 0001, Makarius Wenzel |
Making Isabelle Content Accessible in Knowledge Representation Formats. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway., pp. 1:1-1:24, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-158-0. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Sandra Alves, Delia Kesner, Daniel Ventura |
A Quantitative Understanding of Pattern Matching. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway., pp. 3:1-3:36, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-158-0. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Ambrus Kaposi, András Kovács, Ambroise Lafont |
For Finitary Induction-Induction, Induction Is Enough. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway., pp. 6:1-6:30, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-158-0. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Jesper Cockx |
Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway., pp. 2:1-2:27, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-158-0. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Thorsten Altenkirch, Colin Geniet |
Big Step Normalisation for Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway., pp. 4:1-4:20, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-158-0. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Taichi Uemura |
Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 24th International Conference on Types for Proofs and Programs, TYPES 2018, June 18-21, 2018, Braga, Portugal., pp. 7:1-7:20, 2018, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-106-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Andreas Abel 0001, Fredrik Nordvall Forsberg, Ambrus Kaposi (eds.) |
23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-071-2 The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
1 | Anders Schlichtkrull |
New Formalized Results on the Meta-Theory of a Paraconsistent Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 24th International Conference on Types for Proofs and Programs, TYPES 2018, June 18-21, 2018, Braga, Portugal., pp. 5:1-5:15, 2018, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-106-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Tommaso Petrucciani, Giuseppe Castagna, Davide Ancona, Elena Zucca |
Semantic Subtyping for Non-Strict Languages. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 24th International Conference on Types for Proofs and Programs, TYPES 2018, June 18-21, 2018, Braga, Portugal., pp. 4:1-4:24, 2018, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-106-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | |
Front Matter, Table of Contents, Preface, Conference Organization. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 24th International Conference on Types for Proofs and Programs, TYPES 2018, June 18-21, 2018, Braga, Portugal., pp. 0:1-0:10, 2018, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-106-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Iosif Petrakis |
Dependent Sums and Dependent Products in Bishop's Set Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 24th International Conference on Types for Proofs and Programs, TYPES 2018, June 18-21, 2018, Braga, Portugal., pp. 3:1-3:21, 2018, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-106-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Tarmo Uustalu (eds.) |
21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-030-9 The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
1 | Ulrich Berger 0001, Ralph Matthes, Anton Setzer |
Martin Hofmann's Case for Non-Strictly Positive Data Types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 24th International Conference on Types for Proofs and Programs, TYPES 2018, June 18-21, 2018, Braga, Portugal., pp. 1:1-1:22, 2018, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-106-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Andrej Dudenhefner, Jakob Rehof |
A Simpler Undecidability Proof for System F Inhabitation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 24th International Conference on Types for Proofs and Programs, TYPES 2018, June 18-21, 2018, Braga, Portugal., pp. 2:1-2:11, 2018, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-106-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Filippo Sestini |
Normalization by Evaluation for Typed Weak lambda-Reduction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 24th International Conference on Types for Proofs and Programs, TYPES 2018, June 18-21, 2018, Braga, Portugal., pp. 6:1-6:17, 2018, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-106-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Silvia Ghilezan, Herman Geuvers, Jelena Ivetic (eds.) |
22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1 The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
1 | Guillaume Allais |
Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary, pp. 1:1-1:22, 2017, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-071-2. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Andrej Dudenhefner, Jakob Rehof |
Lower End of the Linial-Post Spectrum. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary, pp. 2:1-2:15, 2017, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-071-2. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | |
Front Matter, Table of Contents, Preface, Conference Organization. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary, pp. 0:i-0:x, 2017, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-071-2. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Ian Orton, Andrew M. Pitts |
Decomposing the Univalence Axiom. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary, pp. 6:1-6:19, 2017, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-071-2. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Julius Michaelis, Tobias Nipkow |
Formalized Proof Systems for Propositional Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary, pp. 5:1-5:16, 2017, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-071-2. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Erik Palmgren |
On Equality of Objects in Categories in Constructive Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary, pp. 7:1-7:7, 2017, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-071-2. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Rodolphe Lepigre |
PML2: Integrated Program Verification in ML. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary, pp. 4:1-4:27, 2017, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-071-2. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Herman Geuvers, Tonny Hurkens |
Proof Terms for Generalized Natural Deduction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary, pp. 3:1-3:39, 2017, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-071-2. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Jacek Chrzaszcz, Aleksy Schubert, Jakub Zakrzewski 0001 |
Coq Support in HAHA. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, pp. 8:1-8:26, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Marc Bezem, Thierry Coquand, Keiko Nakata 0001, Erik Parmann |
Realizability at Work: Separating Two Constructive Notions of Finiteness. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, pp. 6:1-6:23, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Georgiana E. Lungu, Zhaohui Luo |
On Subtyping in Type Theories with Canonical Objects. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, pp. 13:1-13:31, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | 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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, pp. 4:1-4:17, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Bashar Igried, Anton Setzer |
Defining Trace Semantics for CSP-Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, pp. 12:1-12:23, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Robin Adams 0001, Marc Bezem, Thierry Coquand |
A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, pp. 3:1-3:20, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | José Espírito Santo, Maria João Frade, Luís Pinto 0001 |
Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, pp. 10:1-10:27, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Lukasz Czajka 0001 |
A Shallow Embedding of Pure Type Systems into First-Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, pp. 9:1-9:39, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Auke Bart Booij, Martín Hötzel Escardó, Peter LeFanu Lumsdaine, Michael Shulman |
Parametricity, Automorphisms of the Universe, and Excluded Middle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, pp. 7:1-7:14, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | |
Front Matter, Table of Contents, Preface, Conference Organization. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, pp. 0:i-0:x, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Kuen-Bang Hou (Favonia), Robert Harper 0001 |
Covering Spaces in Homotopy Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, pp. 11:1-11:16, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Érik Martin-Dorel, Sergei Soloviev |
A Formal Study of Boolean Games with Random Formulas as Payoff Functions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, pp. 14:1-14:22, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Richard Statman |
The Completeness of BCD for an Operational Semantics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, pp. 15:1-15:5, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, Christopher A. Stone |
Design and Implementation of the Andromeda Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, pp. 5:1-5:31, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Dale Miller 0001 |
Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper). ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, pp. 1:1-1:16, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Simona Ronchi Della Rocca |
Intersection Types and Denotational Semantics: An Extended Abstract (Invited Paper). ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, pp. 2:1-2:7, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg |
Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia, pp. 5:1-5:34, 2015, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-030-9. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Erik Parmann |
Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia, pp. 8:1-8:25, 2015, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-030-9. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Thorsten Altenkirch, Ambrus Kaposi |
Towards a Cubical Type Theory without an Interval. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia, pp. 3:1-3:27, 2015, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-030-9. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Davide Ancona, Paola Giannini, Elena Zucca |
Constrained Polymorphic Types for a Calculus with Name Variables. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia, pp. 4:1-4:29, 2015, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-030-9. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | |
Front Matter, Table of Contents, Preface, Externqal Reviewers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia, pp. 0:i-0:xii, 2015, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-030-9. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Juan Edi, Andrés Viso, Eduardo Bonelli |
Efficient Type Checking for Path Polymorphism. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia, pp. 6:1-6:23, 2015, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-030-9. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Hugo Herbelin, Pierre Letouzey, Matthieu Sozeau (eds.) |
20th International Conference on Types for Proofs and Programs, TYPES 2014, May 12-15, 2014, Paris, France ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-939897-88-0 The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP BibTeX RDF |
|
1 | Robin Adams 0001, Bart Jacobs 0001 |
A Type Theory for Probabilistic and Bayesian Reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia, pp. 1:1-1:34, 2015, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-030-9. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|