Blog posts

• Poltergeist Types2021-04-16T13:37:00Z
• Ceci n'est pas un default2019-03-11T13:37:00Z
• First Cubical Experiment2019-03-06T13:37:00Z
• Instrumenting Total Parsers Written in agdarsec2018-07-13T13:37:00Z
• Three Tricks to make Termination Obvious2016-11-24T13:37:00Z
• Parametrised Modules: (ab)using lambda-lifting2016-01-06T13:37:00Z
• Canonical Structures in Agda using REWRITE2015-08-05T13:37:00Z
• Currying using Canonical Structures2015-07-28T13:37:00Z
• Resource Aware Contexts and Proof Search for ILL2015-03-02T13:37:00Z
• Ever considered using Travis?2015-02-11T13:37:00Z
• Cyclic Lists, Purely2014-08-12T13:37:00Z
• Non-regular Parameters are OK2014-07-17T13:37:00Z
• Lazy Weakening and Equality Test2014-04-28T13:37:00Z
• Dimension-Aware Computations2013-11-02T13:37:00Z
• Glueing terms to models2013-04-30T13:37:00Z
• A universe for syntax with binding2013-04-11T13:37:00Z

Tags cloud

datatype (3) functional programming (7) haskell (2) Agda (10) reflection (3) canonical structures (2) universe (2) coq (2) type safety (2) dependent types (2) binders (2) lambda calculus (3)

---

Last update: 2025 07