Start / Iowa Type Theory Commute / A look at agdas module system

Iowa Type Theory Commute

A look at Agda's module system

14 min • 12 maj 2021

Agda's module system (beautifully described here) could be seen as intermediate between Haskell's and Standard ML's.  It supports nested parametrized modules with information hiding, but does not go all the way to higher-order functors (as in Standard ML).

Senaste avsnitt

Correction: the Correct Author of the Proof from Last Episode, and an AI flop

12 maj | 7 min

Krivine's Proof of FD, Using Intersection Types

5 maj | 22 min

A Measure-Based Proof of Finite Developments

16 april | 23 min

Introduction to the Finite Developments Theorem

27 mars | 16 min

Nominal Isabelle/HOL

31 januari | 16 min
Vad är en podd?

En liten tjänst av I'm With Friends. Finns även på engelska.

Podcastbild

00:00 -00:00
00:00 -00:00