Conor McBride

Proceedings of the 7th Workshop on Mathematically Structured Functional Programming, 2018

2017

Do be do be do.

[BibT_eX]

[DOI]

Sam Lindley

Craig McLaughlin

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Variations on Inductive-Recursive Definitions.

[BibT_eX]

[DOI]

Fredrik Nordvall Forsberg

Stephan Spahn

Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science, 2017

Type-and-scope safe programs and their proofs.

[BibT_eX]

[DOI]

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016

Selected papers from Dependently Typed Programming 2010 - Overview.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2016

I Got Plenty o' Nuttin'.

[BibT_eX]

[DOI]

Proceedings of the A List of Successes That Can Change the World, 2016

2015

Indexed containers.

[BibT_eX]

[DOI]

J. Funct. Program., 2015

Turing-Completeness Totally Free.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction - 12th International Conference, 2015

2014

Transporting functions across ornaments.

[BibT_eX]

[DOI]

J. Funct. Program., 2014

How to keep your neighbours in order.

[BibT_eX]

[DOI]

Conor Thomas McBride

Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, 2014

2013

Small Induction Recursion.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 11th International Conference, 2013

A Categorical Treatment of Ornaments.

[BibT_eX]

[DOI]

Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

Productive coprogramming with guarded recursion.

[BibT_eX]

[DOI]

Robert Atkey

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013

New equations for neutral terms: a sound and complete decision procedure, formalized.

[BibT_eX]

[DOI]

Guillaume Allais

Pierre Boutillier

Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programming, 2013

Hasochism: the pleasure and pain of dependently typed haskell programming.

[BibT_eX]

[DOI]

Sam Lindley

Proceedings of the 2013 ACM SIGPLAN Symposium on Haskell, 2013

2012

Strongly Typed Term Representations in Coq.

[BibT_eX]

[DOI]

J. Autom. Reason., 2012

Elaborating Inductive Definitions

[BibT_eX]

[DOI]

CoRR, 2012

Agda-curious?: an exploration of programming with dependent types.

[BibT_eX]

[DOI]

Conor Thomas McBride

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2012

2011

Dependently Typed Programming (NII Shonan Meeting 2011-3).

[BibT_eX]

[DOI]

Shin-Cheng Mu

Stephanie Weirich

NII Shonan Meet. Rep., 2011

2010

A Tutorial Implementation of a Dependently Typed Lambda Calculus.

[BibT_eX]

[DOI]

Andres Löh

Wouter Swierstra

Fundam. Informaticae, 2010

Djinn, Monotonic.

[BibT_eX]

[DOI]

Proceedings of the Partiality and Recursion in Interactive Theorem Provers, 2010

Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN Workshop on Generic Programming, 2010

Type Inference in Context.

[BibT_eX]

[DOI]

Adam Gundry

Proceedings of the 3rd ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, 2010

The gentle art of levitation.

[BibT_eX]

[DOI]

James Chapman

Peter Morris

Proceedings of the Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, 2010

2009

Preface.

[BibT_eX]

[DOI]

Tarmo Uustalu

J. Funct. Program., 2009

Let's See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Algebra and Coalgebra in Computer Science, 2009

2008

Applicative programming with effects.

[BibT_eX]

[DOI]

Ross Paterson

J. Funct. Program., 2008

Preface.

[BibT_eX]

[DOI]

Venanzio Capretta

Proceedings of the Second Workshop on Mathematically Structured Functional Programming, 2008

Clowns to the left of me, jokers to the right (pearl): dissecting data structures.

[BibT_eX]

[DOI]

Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008

Proving Properties about Lists Using Containers.

[BibT_eX]

[DOI]

Rawle C. S. Prince

Proceedings of the Functional and Logic Programming, 9th International Symposium, 2008

2007

What's the deal with dependent types?

[BibT_eX]

[DOI]

Proceedings of TLDI'07: 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2007

Observational equality, now!

[BibT_eX]

[DOI]

Wouter Swierstra

Proceedings of the ACM Workshop Programming Languages meets Program Verification, 2007

2006

Lego.

[BibT_eX]

[DOI]

Proceedings of the Seventeen Provers of the World, Foreword by Dana S. Scott, 2006

Generic Programming with Dependent Types.

[BibT_eX]

[DOI]

Peter Morris

Proceedings of the Datatype-Generic Programming - International Spring School, 2006

Eliminating Dependent Pattern Matching.

[BibT_eX]

[DOI]

Healfdene Goguen

Proceedings of the Algebra, Meaning, and Computation, 2006

2005

for Data: Differentiating Data Structures.

[BibT_eX]

[DOI]

Michael Gordon Abbott

Fundam. Informaticae, 2005

Epigram reloaded: a standalone typechecker for ETT.

[BibT_eX]

James Chapman

Proceedings of the Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, 2005

2004

The view from the left.

[BibT_eX]

[DOI]

J. Funct. Program., 2004

Exploring the Regular Tree Types.

[BibT_eX]

[DOI]

Peter Morris

Proceedings of the Types for Proofs and Programs, International Workshop, 2004

A Few Constructions on Constructors.

[BibT_eX]

[DOI]

Healfdene Goguen

Proceedings of the Types for Proofs and Programs, International Workshop, 2004

Constructing Polymorphic Programs with Quotient Types.

[BibT_eX]

[DOI]

Michael Gordon Abbott

Proceedings of the Mathematics of Program Construction, 7th International Conference, 2004

Functional pearl: i am not a number-i am a free variable.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN Workshop on Haskell, 2004

Epigram: Practical Programming with Dependent Types.

[BibT_eX]

[DOI]

Proceedings of the Advanced Functional Programming, 2004

2003

First-order unification by structural recursion.

[BibT_eX]

[DOI]

J. Funct. Program., 2003

Inductive Families Need Not Store Their Indices.

[BibT_eX]

[DOI]

Edwin C. Brady

Proceedings of the Types for Proofs and Programs, International Workshop, 2003

Derivatives of Containers.

[BibT_eX]

[DOI]

Michael Gordon Abbott

Proceedings of the Typed Lambda Calculi and Applications, 6th International Conference, 2003

2002

Faking it: Simulating dependent types in Haskell.

[BibT_eX]

[DOI]

J. Funct. Program., 2002

Generic Programming within Dependently Typed Programming.

[BibT_eX]

Proceedings of the Generic Programming, 2002

2000

Dependently typed functional programs and their proofs.

[BibT_eX]

[DOI]

PhD thesis, 2000

Elimination with a Motive.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, International Workshop, 2000

1996

Inverting Inductively Defined Relations in LEGO.

[BibT_eX]

[DOI]