Musing

Faking Linear Variable Usage

Posted on 2021-01-25

idris dependent-types tdd musing

Synthesised or Checked?

Posted on 2021-01-22

idris dependent-types tdd musing

Defining Intrinsically Typed Data Structures

Posted on 2020-08-04

idris dependent-types tdd musing

Programming with Holes

Posted on 2020-07-09

idris dependent-types tdd musing

The Last Step

Posted on 2020-05-26

idris dependent-types tdd musing

Decidably Uninformative

Posted on 2020-05-04

idris dependent-types tdd musing

Mutual Avoidance

Posted on 2020-05-04

idris dependent-types tdd musing

Well-Typed Expressions lead to Well-Typed Well-Scoped Programs

Posted on 2019-12-06

idris dependent-types tdd musing

Hutton's Razor(s)

Posted on 2019-12-04

idris dependent-types tdd musing

On Interfaces and Dependent Types

Posted on 2019-11-20

idris dependent-types tdd musing