| 24th International Conference on Types for Proofs and Programs, TYPES 2018, June 18-21, 2018, Braga, Portugal. | 0 | 0.34 | 2019 |
| Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version). | 1 | 0.37 | 2017 |
| Special issue on Programming with Dependent Types Editorial. | 0 | 0.34 | 2017 |
| Game Semantics and Normalization by Evaluation. | 0 | 0.34 | 2015 |
| Combining interactive and automatic reasoning in first order theories of functional programs | 3 | 0.40 | 2012 |
| Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation. | 2 | 0.38 | 2012 |
| Agda Implementors Meeting (NII Shonan Meeting 2011-2). | 0 | 0.34 | 2011 |
| The biequivalence of locally cartesian closed categories and Martin-Löf type theories. | 4 | 0.67 | 2011 |
| Embedding a logical theory of constructions in Agda | 3 | 0.39 | 2009 |
| A Brief Overview of Agda --- A Functional Language with Dependent Types | 77 | 2.64 | 2009 |
| On the algebraic foundation of proof assistants for intuitionistic type theory | 4 | 0.52 | 2008 |
| Towards Formalizing Categorical Models of Type Theory in Type Theory | 8 | 0.68 | 2008 |
| The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories -- an Intuitionistic Perspective | 2 | 0.47 | 2008 |
| Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory | 2 | 0.47 | 2008 |
| Dependent Types at Work | 16 | 1.35 | 2008 |
| Normalization by Evaluation for Martin-Löf Type Theory with One Universe | 7 | 0.58 | 2007 |
| Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements | 15 | 1.02 | 2007 |
| Indexed induction–recursion | 18 | 1.40 | 2006 |
| Verifying Haskell programs by combining testing, model checking and interactive theorem proving | 8 | 0.53 | 2004 |
| Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming | 0 | 0.34 | 2004 |
| Random generators for dependent types | 1 | 0.36 | 2004 |
| Combining Testing and Proving in Dependent Type Theory | 26 | 1.31 | 2003 |
| Universes for generic programs and proofs in dependent type theory | 42 | 2.09 | 2003 |
| Induction–recursion and initial algebras | 18 | 1.28 | 2003 |
| Verifying Haskell Programs by Combining Testing and Proving | 4 | 0.49 | 2003 |
| Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures | 7 | 0.59 | 2002 |
| A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory | 23 | 2.55 | 2000 |
| Types for Proofs and Programs, International Workshop TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers | 10 | 1.45 | 2000 |
| Normalization and Partial Evaluation | 19 | 0.99 | 2000 |
| Normalization and the Yoneda embedding | 22 | 1.74 | 1998 |
| Intuitionistic model constructions and normalization proofs | 48 | 5.42 | 1997 |
| Representing inductively defined sets by wellorderings in Martin-Löf's type theory | 16 | 2.29 | 1997 |
| A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem | 2 | 0.81 | 1996 |
| Extracting a Proof of Coherence for Monoidal Categories from a Proof of Normalization for Monoids | 12 | 1.77 | 1995 |
| Internal Type Theory | 27 | 3.67 | 1995 |
| Types for Proofs and Programs, International Workshop TYPES'94, Båstad, Sweden, June 6-10, 1994, Selected Papers | 11 | 3.57 | 1995 |
| Inductive Families | 23 | 2.63 | 1994 |
| Inductive Definitions and Type Theory: an Introduction (Preliminary Version) | 6 | 0.53 | 1994 |
| Inverse image analysis generalises strictness analysis | 15 | 0.97 | 1991 |
| Category Theory and Computer Science, Manchester, UK, September 5-8, 1989, Proceedings | 22 | 24.83 | 1989 |
| Program verification in a logical theory of construction | 11 | 2.09 | 1985 |
| Category Theory and Programming Language Semantics: an Overview | 2 | 0.41 | 1985 |
| Domain Algebras | 2 | 0.95 | 1984 |
| Some Results On The Deductive Structure Of Join Dependencies | 0 | 0.34 | 1984 |
| Towards a Unified Theory of Data Types: Some Categorical Aspects | 1 | 0.34 | 1983 |
