dot-iris
Type verification library
Mechanized formalization of soundness for DOT with logical relations in Coq
Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization
30 stars
5 watching
1 forks
Language: HTML
last commit: 16 days ago coqcoq-formalizationcoq-formalizationsdot-calculuspapersoundnesstype-theory
Related projects:
| Repository | Description | Stars |
|---|---|---|
 samuelgruetter/dot-calculus | A formalization of Dependent Object Types (DOT) calculus in Coq to support type safety proofs for a new foundation for Scala's type system | 62 |
 namin/dot | Mechanized proof of soundness for a type-theoretic foundation for languages like Scala | 154 |
 tchajed/iris-simp-lang | Instantiates a simple programming language with Iris to verify concurrent separation logic programs | 49 |
 reynir/brainfuck | Formalizing Brainfuck in Coq to prove its properties and verify a compiler for simple arithmetic expressions. | 26 |
 fblanqui/color | A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination. | 35 |
 bedrocksystems/brick | Formalization of C++ logic for verifying concurrent programming | 69 |
 rafaelcgs10/w-in-coq | A Coq formalization of Damas-Milner type system and its algorithm W for verifying the correctness of type inference tools. | 25 |
 lysxia/system-f | A formalization of polymorphic lambda calculus with a proof of parametricity theorem. | 33 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 291 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 442 |
 mit-plv/fiat | A Coq-based library for synthesizing correct-by-construction abstract data types and parsers from formal specifications | 147 |
 verse-lab/ceramist | A verified hash-based approximate membership structure library in Coq | 121 |
 formal-land/coq-of-python | Formal verification of Python code using Coq | 30 |
 xavierleroy/cdf-mech-sem | Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |