189
click to vote
CPP
10 years 25 days ago
2016 
In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing rec...
116
click to vote
CPP
10 years 25 days ago
2016
In Separation Logic, representation predicates are used to describe mutable data structures, by establishing a relationship between the entry point of the structure, the piece of ...
CPP
10 years 25 days ago
2016
This papers extends the Nuprl proof assistant (a system representative of the class of extensional type theories `a la Martin-L¨of) with named exceptions and handlers, as well as...
|
Artificial Intelligence