gallais/generic-syntax

A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs

Agda

548 commits

updated Mar 5, 2022

gallais.github.io/generic-syntax/Generic.html

See the code

README

generic-syntax

A self-contained repository for the paper A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs

Typechecking

To check this development, you'll need:

Agda 2.6.1.3
Agda's Standard Library 1.5

agda

generic-programming

proof

semantic

Contributors

399 commits

77 commits

49 commits

21 commits

Similar repos

gallais/agdarsec

Total Parser Combinators in Agda

136

same org

0xd34df00d/refinedt

Refinement types + dependent types = ❤️

jyp/nano-Agda

Tiny type-checker with dependent types

digama0/lean-type-theory

LaTeX code for a paper on lean's type theory

171

jespercockx/agda-lecture-notes

Agda lecture notes for the Functional Programming course at TU Delft

135

agda/agda

Agda is a dependently typed programming language / interactive theorem prover.

2,930

Andromedans/andromeda

A proof assistant for general type theories

317

HigherOrderCO/Kind

A modern proof language

3,762

Languages

Agda

99.2%

gallais/generic-syntax

A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs

Agda

548 commits

updated Mar 5, 2022

gallais.github.io/generic-syntax/Generic.html

See the code

README

generic-syntax

A self-contained repository for the paper A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs

Typechecking

To check this development, you'll need:

Agda 2.6.1.3
Agda's Standard Library 1.5

agda

generic-programming

proof

semantic

Similar repos

gallais/agdarsec

Total Parser Combinators in Agda

136

same org

0xd34df00d/refinedt

Refinement types + dependent types = ❤️

jyp/nano-Agda

Tiny type-checker with dependent types

digama0/lean-type-theory

LaTeX code for a paper on lean's type theory

171

jespercockx/agda-lecture-notes

Agda lecture notes for the Functional Programming course at TU Delft

135

agda/agda

Agda is a dependently typed programming language / interactive theorem prover.

2,930

Andromedans/andromeda

A proof assistant for general type theories

317

HigherOrderCO/Kind

A modern proof language

3,762

Contributors

399 commits

77 commits

49 commits

21 commits

Languages

Agda

99.2%