racting these leads us to introduce the notion of a path object category. This is a relatively simple axiomatic framework, which is nonetheless sufficiently strong to allow the con...
Sized types are a modular and theoretically well-understood tool for checking termination of recursive and productivity of corecursive definitions. The essential idea is to track ...
We describe how a set-theoretic foundation for mathematics can be encoded in the new system Scunak. We then discuss an encoding of the construction of functions as functional relat...
We present a type system extending the dependent type theory LF, whose terms are more amenable to compact representation. This is achieved by carefully omitting certain subterms w...
This note is about work in progress on the topic of "internal type theory" where we investigate the internal formalization of the categorical metatheory of constructive ...
We present a denotational model of impredicative Hoare Type Theory, a very expressive dependent type theory in which one can and reason about mutable abstract data types. The model...
Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksan...
We introduce basic concepts from object-oriented programming into dependent type theory based on the idea of modelling objects as interactive programs. We consider methods, interf...
We consider the problem of providing formal support for working tract syntax involving variable binders. Gabbay and Pitts have shown in their work on Fraenkel-Mostowski (FM) set th...
Abstract. We have formalized material from an introductory real analysis textbook in the proof assistant Scunak. Scunak is a system based on set theory encoded in a dependent type ...
Abstract. Type Classes have met a large success in Haskell and Isabelle, as a solution for sharing notations by overloading and for specith abstract structures by quantification o...