New modular approach to formalizing complex types in type theory

by Aleksey Nogin
2000-2001

I will present a new modular approach to formalizing complex types in type theory, in particular - the quotient type. I will show how the new building blocks that I create for the quotient type can be successfully reused for other purposes, in particular - to formalize Mark's collection types.

New modular approach to formalizing complex types in type theory

by Aleksey Nogin 2000-2001

by Aleksey Nogin
2000-2001