| A type- and scope-safe universe of syntaxes with binding: their semantics and proofs | 0 | 0.34 | 2021 |
| Doo bee doo bee doo | 0 | 0.34 | 2020 |
| A type and scope safe universe of syntaxes with binding: their semantics and proofs | 2 | 0.36 | 2018 |
| Everybody's Got To Be Somewhere. | 1 | 0.35 | 2018 |
| Variations on Inductive-Recursive Definitions. | 0 | 0.34 | 2017 |
| Type-and-scope safe programs and their proofs. | 5 | 0.45 | 2017 |
| I Got Plenty o' Nuttin'. | 5 | 0.45 | 2016 |
| Do Be Do Be Do | 0 | 0.34 | 2016 |
| Selected papers from Dependently Typed Programming 2010 - Overview. | 0 | 0.34 | 2016 |
| Turing-Completeness Totally Free | 7 | 0.44 | 2015 |
| Indexed Containers | 16 | 0.80 | 2015 |
| A Categorical Treatment of Ornaments | 5 | 0.56 | 2013 |
| New equations for neutral terms: a sound and complete decision procedure, formalized | 1 | 0.35 | 2013 |
| Small Induction Recursion. | 3 | 0.42 | 2013 |
| Productive coprogramming with guarded recursion | 31 | 1.12 | 2013 |
| Hasochism: the pleasure and pain of dependently typed haskell programming | 20 | 1.10 | 2013 |
| Strongly Typed Term Representations in Coq | 25 | 1.00 | 2012 |
| Transporting functions across ornaments | 11 | 0.69 | 2012 |
| Agda-curious?: an exploration of programming with dependent types | 3 | 0.42 | 2012 |
| Elaborating Inductive Definitions | 0 | 0.34 | 2012 |
| Dependently Typed Programming (NII Shonan Meeting 2011-3). | 0 | 0.34 | 2011 |
| A Tutorial Implementation of a Dependently Typed Lambda Calculus | 13 | 0.91 | 2010 |
| Type inference in context | 1 | 0.36 | 2010 |
| Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation | 8 | 0.57 | 2010 |
| Djinn, Monotonic. | 0 | 0.34 | 2010 |
| Let's See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract) | 4 | 0.43 | 2009 |
| Proving properties about lists using containers | 6 | 0.61 | 2008 |
| Applicative programming with effects | 124 | 4.96 | 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 |
| What's the deal with dependent types? | 0 | 0.34 | 2007 |
| Generic Programming with Dependent Types | 13 | 0.82 | 2006 |
| Lego | 0 | 0.34 | 2006 |
| for Data: Differentiating Data Structures | 1 | 0.37 | 2005 |
| Epigram Reloaded: A Standalone Typechecker for {ETT | 10 | 0.92 | 2005 |
| The view from the left | 122 | 6.39 | 2004 |
| Constructing Polymorphic Programs with Quotient Types | 12 | 0.82 | 2004 |
| A few constructions on constructors | 11 | 1.20 | 2004 |
| Exploring the regular tree types | 15 | 0.80 | 2004 |
| Epigram: practical programming with dependent types | 47 | 2.04 | 2004 |
| Functional pearl: i am not a number--i am a free variable | 20 | 1.23 | 2004 |
| Inductive Families Need Not Store Their Indices | 35 | 1.76 | 2003 |
| Derivatives of Containers | 16 | 1.61 | 2003 |
| First-order unification by structural recursion | 13 | 1.17 | 2003 |
| Faking it Simulating dependent types in Haskell | 45 | 2.39 | 2002 |
| Generic Programming within Dependently Typed Programming | 50 | 2.40 | 2002 |
| Inverting Inductively Defined Relations in LEGO | 7 | 1.04 | 1996 |
