| 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  |
TYPES  |
2023 |
DBLP BibTeX RDF |
|
| 1 | Luca Padovani |
On the Fair Termination of Client-Server Sessions. |
TYPES |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Philipp Stassen, Daniel Gratzer, Lars Birkedal |
{mitten}: A Flexible Multimodal Proof Assistant. |
TYPES |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Catherine Dubois, Nicolas Magaud, Alain Giorgetti |
Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families. |
TYPES |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrea Colledan, Ugo Dal Lago |
On Dynamic Lifting and Effect Typing in Circuit Description Languages. |
TYPES |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Max Zeuner, Anders Mörtberg |
A Univalent Formalization of Constructive Affine Schemes. |
TYPES |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Fábio Reis, Sandra Alves, Mário Florido |
Linear Rank Intersection Types. |
TYPES |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó |
Type Theory with Explicit Universe Polymorphism. |
TYPES |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Amélie Ledein, Valentin Blot, Catherine Dubois |
A Semantics of |
TYPES |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Tonny Hurkens |
Classical Natural Deduction from Truth Tables. |
TYPES |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Dominic P. Mulligan |
All Watched Over by Machines of Loving Grace. |
TYPES |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Émilie Grienenberger |
Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory. |
TYPES |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tamás Végh |
The Münchhausen Method in Type Theory. |
TYPES |
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). |
TYPES |
2022 |
DBLP BibTeX RDF |
|
| 1 | Nathan Mull |
An Irrelevancy-Eliminating Translation of Pure Type Systems. |
TYPES |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Felix Bradley, Zhaohui Luo |
A Metatheoretic Analysis of Subtype Universes. |
TYPES |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Kobe Wullaert, Ralph Matthes, Benedikt Ahrens |
Univalent Monoidal Categories. |
TYPES |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | |
Front Matter, Table of Contents, Preface, Conference Organization. |
TYPES |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Giulio Fellin, Sara Negri, Eugenio Orlandelli |
Constructive Cut Elimination in Geometric Logic. |
TYPES |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Yuta Takahashi |
Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus. |
TYPES |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Georgi Nakov, Fredrik Nordvall Forsberg |
Quantitative Polynomial Functors. |
TYPES |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Thibaut Benjamin |
Formalisation of Dependent Type Theory: The Example of CaTT. |
TYPES |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | |
Front Matter, Table of Contents, Preface, Conference Organization. |
TYPES |
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. |
TYPES |
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. |
TYPES |
2021 |
DBLP BibTeX RDF |
|
| 1 | Pietro Di Gianantonio, Marina Lenisa |
Principal Types as Lambda Nets. |
TYPES |
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. |
TYPES |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Asta Halkjær From |
A Succinct Formalization of the Completeness of First-Order Logic. |
TYPES |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Christa Jenkins, Andrew Marmaduke, Aaron Stump |
Simulating Large Eliminations in Cedille. |
TYPES |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | István Donkó, Ambrus Kaposi |
Internal Strict Propositions Using Point-Free Equations. |
TYPES |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Rafaël Bocquet |
Strictification of Weakly Stable Type-Theoretic Structures Using Generic Contexts. |
TYPES |
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. |
TYPES |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Abel 0001 |
On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction. |
TYPES |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Matteo Manighetti, Dale Miller 0001, Alberto Momigliano |
Two Applications of Logic Programming to Coq. |
TYPES |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Furio Honsell, Marina Lenisa, Ivan Scagnetto |
Λ-Symsym: An Interactive Tool for Playing with Involutions and Types. |
TYPES |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Reynald Affeldt, David Nowak |
Extending Equational Monadic Reasoning with Monad Transformers. |
TYPES |
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. |
TYPES |
2020 |
DBLP BibTeX RDF |
|
| 1 | |
Front Matter, Table of Contents, Preface, Conference Organization. |
TYPES |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Pawel Urzyczyn |
Duality in Intuitionistic Propositional Logic. |
TYPES |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Harry Maclean, Zhaohui Luo |
Subtype Universes. |
TYPES |
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. |
TYPES |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Jasper Hugunin |
Why Not W? |
TYPES |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Gabriel Hondet, Frédéric Blanqui |
Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory. |
TYPES |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Asta Halkjær From |
Synthetic Completeness for a Terminating Seligman-Style Tableau System. |
TYPES |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Guido De Luca, Carlos Luna 0001 |
Towards a Certified Reference Monitor of the Android 10 Permission System. |
TYPES |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, Stephanie Weirich |
Eta-Equivalence in Core Dependent Haskell. |
TYPES |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Nils Anders Danielsson |
Higher Inductive Type Eliminators Without Paths. |
TYPES |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | |
Front Matter, Table of Contents, Preface, Conference Organization. |
TYPES |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefano Piceghello |
Coherence for Monoidal Groupoids in HoTT. |
TYPES |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Gun Pinyo, Nicolai Kraus |
From Cubes to Twisted Cubes via Graph Morphisms in Type Theory. |
TYPES |
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. |
TYPES |
2019 |
DBLP BibTeX RDF |
|
| 1 | Stefan Monnier, Nathaniel Bos |
Is Impredicativity Implicitly Implicit? |
TYPES |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Kohlhase, Florian Rabe 0001, Makarius Wenzel |
Making Isabelle Content Accessible in Knowledge Representation Formats. |
TYPES |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Sandra Alves, Delia Kesner, Daniel Ventura |
A Quantitative Understanding of Pattern Matching. |
TYPES |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Ambrus Kaposi, András Kovács, Ambroise Lafont |
For Finitary Induction-Induction, Induction Is Enough. |
TYPES |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Jesper Cockx |
Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules. |
TYPES |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Thorsten Altenkirch, Colin Geniet |
Big Step Normalisation for Type Theory. |
TYPES |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Taichi Uemura |
Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing. |
TYPES |
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 |
TYPES |
2018 |
DBLP BibTeX RDF |
|
| 1 | Anders Schlichtkrull |
New Formalized Results on the Meta-Theory of a Paraconsistent Logic. |
TYPES |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Tommaso Petrucciani, Giuseppe Castagna, Davide Ancona, Elena Zucca |
Semantic Subtyping for Non-Strict Languages. |
TYPES |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | |
Front Matter, Table of Contents, Preface, Conference Organization. |
TYPES |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Iosif Petrakis |
Dependent Sums and Dependent Products in Bishop's Set Theory. |
TYPES |
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 |
TYPES |
2018 |
DBLP BibTeX RDF |
|
| 1 | Ulrich Berger 0001, Ralph Matthes, Anton Setzer |
Martin Hofmann's Case for Non-Strictly Positive Data Types. |
TYPES |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrej Dudenhefner, Jakob Rehof |
A Simpler Undecidability Proof for System F Inhabitation. |
TYPES |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Filippo Sestini |
Normalization by Evaluation for Typed Weak lambda-Reduction. |
TYPES |
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 |
TYPES |
2018 |
DBLP BibTeX RDF |
|
| 1 | Guillaume Allais |
Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic. |
TYPES |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrej Dudenhefner, Jakob Rehof |
Lower End of the Linial-Post Spectrum. |
TYPES |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | |
Front Matter, Table of Contents, Preface, Conference Organization. |
TYPES |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Ian Orton, Andrew M. Pitts |
Decomposing the Univalence Axiom. |
TYPES |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Julius Michaelis, Tobias Nipkow |
Formalized Proof Systems for Propositional Logic. |
TYPES |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Erik Palmgren |
On Equality of Objects in Categories in Constructive Type Theory. |
TYPES |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Rodolphe Lepigre |
PML2: Integrated Program Verification in ML. |
TYPES |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Tonny Hurkens |
Proof Terms for Generalized Natural Deduction. |
TYPES |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Jacek Chrzaszcz, Aleksy Schubert, Jakub Zakrzewski 0001 |
Coq Support in HAHA. |
TYPES |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Marc Bezem, Thierry Coquand, Keiko Nakata 0001, Erik Parmann |
Realizability at Work: Separating Two Constructive Notions of Finiteness. |
TYPES |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Georgiana E. Lungu, Zhaohui Luo |
On Subtyping in Type Theories with Canonical Objects. |
TYPES |
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. |
TYPES |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Bashar Igried, Anton Setzer |
Defining Trace Semantics for CSP-Agda. |
TYPES |
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. |
TYPES |
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. |
TYPES |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Lukasz Czajka 0001 |
A Shallow Embedding of Pure Type Systems into First-Order Logic. |
TYPES |
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. |
TYPES |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | |
Front Matter, Table of Contents, Preface, Conference Organization. |
TYPES |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Kuen-Bang Hou (Favonia), Robert Harper 0001 |
Covering Spaces in Homotopy Type Theory. |
TYPES |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Érik Martin-Dorel, Sergei Soloviev |
A Formal Study of Boolean Games with Random Formulas as Payoff Functions. |
TYPES |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Richard Statman |
The Completeness of BCD for an Operational Semantics. |
TYPES |
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. |
TYPES |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Dale Miller 0001 |
Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper). |
TYPES |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Simona Ronchi Della Rocca |
Intersection Types and Denotational Semantics: An Extended Abstract (Invited Paper). |
TYPES |
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. |
TYPES |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Erik Parmann |
Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation. |
TYPES |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Thorsten Altenkirch, Ambrus Kaposi |
Towards a Cubical Type Theory without an Interval. |
TYPES |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Davide Ancona, Paola Giannini, Elena Zucca |
Constrained Polymorphic Types for a Calculus with Name Variables. |
TYPES |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | |
Front Matter, Table of Contents, Preface, Externqal Reviewers. |
TYPES |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Juan Edi, Andrés Viso, Eduardo Bonelli |
Efficient Type Checking for Path Polymorphism. |
TYPES |
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 |
TYPES |
2015 |
DBLP BibTeX RDF |
|
| 1 | Robin Adams 0001, Bart Jacobs 0001 |
A Type Theory for Probabilistic and Bayesian Reasoning. |
TYPES |
2015 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license