| 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy. | 0 | 0.34 | 2021 |
| Constructing a universe for the setoid model. | 0 | 0.34 | 2021 |
| Martin Hofmann's contributions to type theory: Groupoids and univalence. | 0 | 0.34 | 2021 |
| The Integers as a Higher Inductive Type | 0 | 0.34 | 2020 |
| Constructing quotient inductive-inductive types. | 1 | 0.37 | 2019 |
| Big Step Normalisation for Type Theory. | 0 | 0.34 | 2019 |
| Setoid Type Theory - A Syntactic Translation. | 0 | 0.34 | 2019 |
| Quotient inductive-inductive types. | 0 | 0.34 | 2018 |
| Free Higher Groups in Homotopy Type Theory. | 1 | 0.35 | 2018 |
| Pure Functional Epidemics: An Agent-Based Approach | 0 | 0.34 | 2018 |
| Quotient Inductive-Inductive Types. | 0 | 0.34 | 2018 |
| Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type. | 5 | 0.50 | 2017 |
| Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type. | 0 | 0.34 | 2017 |
| Normalisation by Evaluation for Type Theory, in Type Theory. | 0 | 0.34 | 2017 |
| Normalisation by Evaluation for Dependent Types. | 2 | 0.37 | 2016 |
| Type theory in type theory using quotient inductive types. | 10 | 0.75 | 2016 |
| Extending Homotopy Type Theory with Strict Equality. | 7 | 0.63 | 2016 |
| Notions of Anonymous Existence in Martin-Löf Type Theory. | 0 | 0.34 | 2016 |
| Selected papers from Dependently Typed Programming 2010 - Overview. | 0 | 0.34 | 2016 |
| Indexed Containers | 16 | 0.80 | 2015 |
| Towards a Cubical Type Theory without an Interval. | 0 | 0.34 | 2015 |
| Relative Monads Formalised | 0 | 0.34 | 2014 |
| Some constructions on ω-groupoids | 0 | 0.34 | 2014 |
| Generalizations of Hedberg's Theorem. | 4 | 0.63 | 2013 |
| Small Induction Recursion. | 3 | 0.42 | 2013 |
| A Syntactical Approach to Weak omega-Groupoids. | 0 | 0.34 | 2012 |
| A categorical semantics for inductive-inductive definitions | 3 | 0.45 | 2011 |
| A Partial Type Checking Algorithm for Type: Type | 1 | 0.40 | 2011 |
| Hereditary substitutions for simple types, formalized | 6 | 0.47 | 2010 |
| Monads need not be endofunctors. | 15 | 0.94 | 2010 |
| Termination Checking in the Presence of Nested Inductive and Coinductive Types. | 6 | 0.50 | 2010 |
| Subtyping, Declaratively | 2 | 0.38 | 2010 |
| PiSigma: Dependent Types without the Sugar | 5 | 0.46 | 2010 |
| Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009 | 8 | 0.88 | 2009 |
| Big-step normalisation | 4 | 0.51 | 2009 |
| A Universe Of Strictly Positive Families | 5 | 0.48 | 2009 |
| More dependent types for distributed arrays | 5 | 0.57 | 2008 |
| From Reversible to Irreversible Computations | 2 | 0.41 | 2008 |
| Observational equality, now! | 29 | 1.70 | 2007 |
| Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers | 15 | 1.51 | 2007 |
| An Algebra of Pure Quantum Programming | 15 | 0.93 | 2007 |
| Tait in one big step | 4 | 0.58 | 2006 |
| Generic Programming with Dependent Types | 13 | 0.82 | 2006 |
| Containers: constructing strictly positive types | 55 | 2.34 | 2005 |
| for Data: Differentiating Data Structures | 1 | 0.37 | 2005 |
| Structuring quantum effects: superoperators as arrows | 21 | 1.11 | 2005 |
| Epigram Reloaded: A Standalone Typechecker for {ETT | 10 | 0.92 | 2005 |
| Constructing Polymorphic Programs with Quotient Types | 12 | 0.82 | 2004 |
| Normalization by Evaluation for lambda-2. | 1 | 0.36 | 2004 |
| 04381 Abstracts Collection - Dependently Typed Programming. | 0 | 0.34 | 2004 |
