Blog posts with tag "Agda"

• First Cubical Experiment2019-03-06
• Instrumenting Total Parsers Written in agdarsec2018-07-13
• Three Tricks to make Termination Obvious2016-11-24
• Parametrised Modules: (ab)using lambda-lifting2016-01-06
• Canonical Structures in Agda using REWRITE2015-08-05
• Currying using Canonical Structures2015-07-28
• Non-regular Parameters are OK2014-07-17
• Dimension-Aware Computations2013-11-02
• Glueing terms to models2013-04-30
• A universe for syntax with binding2013-04-11

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: 2024 04