samuelgruetter/dot-calculus

Formalization of the Dependent Object Types (DOT) calculus

Coq

953 commits

updated Aug 30, 2022

See the code

README

Dependent Object Types (DOT)

The DOT calculus proposes a new foundation for Scala's type system.

DOT has been presented at the FOOL 2012 workshop (PDF).

We now have several mechanized type safety proofs. This repo implements the wadlerfest model in Coq, based on previous work in the namin/dot and TiarkRompf/minidot repos.

Installation

Works in Coq 8.4.6 and OCaml 4.02.3.

opam switch create with-wadlerfest-dot 4.02.3
eval $(opam env)
opam pin add coq 8.4.6

Then, run make from the ln directory.

Contributors

samuelgruetter

629 commits

namin

323 commits

aha66

1 commits

Similar repos

TiarkRompf/minidot

Dependent Object Types (DOT), bottom up

ott-lang/ott

The Ott tool for writing definitions of programming languages and calculi

422

rocq-archive/coq-in-coq

A formalisation of the Calculus of Constructions

coq-contribs/coq-in-coq

A formalisation of the Calculus of Constructions

JBakouny/Scallina

A Coq-based synthesis of Scala programs which are correct-by-construction

coq/coq

The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language…

5,586

IBM/FormalML

Formalization of Machine Learning Theory with Applications to Program Synthesis

HigherOrderCO/Kind

A modern proof language

3,762

Languages

Coq

98.9%

samuelgruetter/dot-calculus

Formalization of the Dependent Object Types (DOT) calculus

Coq

953 commits

updated Aug 30, 2022

See the code

README

Dependent Object Types (DOT)

The DOT calculus proposes a new foundation for Scala's type system.

DOT has been presented at the FOOL 2012 workshop (PDF).

We now have several mechanized type safety proofs. This repo implements the wadlerfest model in Coq, based on previous work in the namin/dot and TiarkRompf/minidot repos.

Installation

Works in Coq 8.4.6 and OCaml 4.02.3.

opam switch create with-wadlerfest-dot 4.02.3
eval $(opam env)
opam pin add coq 8.4.6

Then, run make from the ln directory.

Similar repos

TiarkRompf/minidot

Dependent Object Types (DOT), bottom up

ott-lang/ott

The Ott tool for writing definitions of programming languages and calculi

422

rocq-archive/coq-in-coq

A formalisation of the Calculus of Constructions

coq-contribs/coq-in-coq

A formalisation of the Calculus of Constructions

JBakouny/Scallina

A Coq-based synthesis of Scala programs which are correct-by-construction

coq/coq

The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language…

5,586

IBM/FormalML

Formalization of Machine Learning Theory with Applications to Program Synthesis

HigherOrderCO/Kind

A modern proof language

3,762

Contributors

samuelgruetter

629 commits

namin

323 commits

aha66

1 commits

Languages

Coq

98.9%