The DOT Calculus and its Variations

A good proof is one that makes us wiser. -- Yuri Manin

Formalizations of the Dependent Object Types (DOT) calculus, from the bottom up, with soundness proofs at each step.

Towards Strong Normalization for Dependent Object Types (ECOOP'17) [pdf]
- D<:> with extensions
From F to DOT: Type Soundness Proofs with Definitional Interpreters (POPL'17) [pdf]
Type Soundness for Dependent Object Types (OOPSLA'16) [pdf]
- DOT in small-step
Foundations of Path-Dependent Types (OOPSLA'14) [pdf]
- muDOT

Name		Name	Last commit message	Last commit date
Latest commit History 3,171 Commits
.io.livecode.ch		.io.livecode.ch
dev2013		dev2013
dev2014		dev2014
dev2015		dev2015
dev2016		dev2016
dev2017		dev2017
doc2014		doc2014
doc2015		doc2015
ecoop17		ecoop17
old		old
oopsla14		oopsla14
oopsla16		oopsla16
popl17		popl17
.gitignore		.gitignore
README.md		README.md

Provide feedback