| Abstracting extensible data types: or, rows by any other name. | 0 | 0.34 | 2019 |
| A type and scope safe universe of syntaxes with binding: their semantics and proofs | 2 | 0.36 | 2018 |
| Triangulating context lemmas. | 0 | 0.34 | 2018 |
| On principles of Least Change and Least Surprise for bidirectional transformations. | 1 | 0.36 | 2017 |
| Type-and-scope safe programs and their proofs. | 5 | 0.45 | 2017 |
| Introduction to Bidirectional Transformations. | 0 | 0.34 | 2016 |
| How to Regain Equilibrium without Losing your Balance? Scenarios for Bx Deployment (Discussion Paper). | 0 | 0.34 | 2016 |
| Complements Witness Consistency. | 2 | 0.37 | 2016 |
| Reflections on Monadic Lenses | 1 | 0.35 | 2016 |
| Bidirectional Transformations with Deltas: A Dependently Typed Approach (Talk Proposal). | 0 | 0.34 | 2016 |
| Notions of Bidirectional Computation and Entangled State Monads | 10 | 0.74 | 2015 |
| Towards a Principle of Least Surprise for Bidirectional Transformations | 4 | 0.51 | 2015 |
| Coalgebraic Aspects of Bidirectional Computation | 0 | 0.34 | 2015 |
| Towards a Repository of Bx Examples. | 9 | 0.61 | 2014 |
| Entangled State Monads. | 0 | 0.34 | 2014 |
| The λμT-calculus. | 1 | 0.36 | 2013 |
| The lambda-mu-T-calculus | 1 | 0.36 | 2012 |
| Narrating Formal Proof (Work in Progress) | 1 | 0.52 | 2012 |
| A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems | 11 | 0.66 | 2011 |
| Dynamic Proof Pages. | 2 | 0.38 | 2011 |
| Proviola: a tool for proof re-animation | 10 | 1.07 | 2010 |
| Type inference in context | 1 | 0.36 | 2010 |
| Pure Type Systems Without Explicit Contexts | 2 | 0.42 | 2010 |
| Domain Specific Languages (DSLs) for Network Protocols (Position Paper) | 5 | 0.51 | 2009 |
| A Logically Saturated Extension of lambdaµµ. | 0 | 0.34 | 2009 |
| Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle | 0 | 0.34 | 2008 |
| A Real Semantic Web for Mathematics Deserves a Real Semantics | 1 | 0.37 | 2008 |
| A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq | 3 | 0.44 | 2008 |
| Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types. | 2 | 0.41 | 2007 |
| A sequent calculus for type theory | 5 | 0.44 | 2006 |
| Why dependent types matter | 28 | 1.82 | 2006 |
| The view from the left | 122 | 6.39 | 2004 |
| A few constructions on constructors | 11 | 1.20 | 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 |
| Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers | 12 | 2.68 | 2002 |
| Some Lambda Calculus and Type Theory Formalized | 51 | 3.11 | 1999 |
| Checking algorithms for pure type systems | 27 | 3.07 | 1993 |
| Pure Type Systems Formalized | 49 | 5.71 | 1993 |
| Deliverables: A Categorial Approach to Program Development in Type Theory | 30 | 2.95 | 1993 |
