On 31/03/17 05:34, Tim Daly wrote:
Consider the Axiom Domain NonNegativeInteger. NNI roughly
corresponds to the Type theory "Nat" construction. They differ
in that Axiom uses Lisp Integers whereas Type theory uses
Peano arithmetic (a zero and a successor function) but for
our purposes this does n
I've spent a lot of time talking to professors at CMU about
Type Theory and the Curry-Howard correspondence. There
are excellent lectures online, taught every summer in Oregon.
https://www.cs.uoregon.edu/research/summerschool/summer16/curriculum.php
Type theory has advanced considerably in recent
