tealeaves
Syntax framework
A framework for abstract syntactical reasoning in Coq.
A Coq library for abstract syntactical reasoning
23 stars
3 watching
0 forks
Language: Coq
last commit: 4 months ago coqsyntaxvariable-binding
Related projects:
Repository | Description | Stars |
---|---|---|
uds-psl/autosubst2 | A tool for generating Coq code from syntactic theories with variable binders | 17 |
korpling/salt | A flexible data model and API for representing linguistic data in a language-independent and theory-neutral way. | 15 |
uwplse/structtact | A Coq library providing structural tactics and utility definitions to simplify proof development in proof assistants. | 21 |
distributedcomponents/disel | A framework for implementing and verifying distributed systems using Coq | 95 |
coq-community/semantics | A comprehensive survey of programming language semantics styles implemented in Coq | 46 |
ssprove/ssprove | A foundational framework for modular cryptographic proofs in Coq | 56 |
sang-hyeon/plastic | Provides encapsulation of domain logic and business rules in an application layer using the Command pattern and source generator. | 59 |
ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 153 |
discus-lang/iron | Formalizations of functional languages with a focus on proof and verification | 142 |
tezos/tezoscoq | A Coq-based library providing a formal verification framework for the Tezos smart contract language | 28 |
heades/system-f-coq | An implementation of System F in Coq, aiming to provide a rigorous and expressive formal system for describing programming languages. | 19 |
rabbibotton/clog | A GUI framework that enables web-based graphical user interfaces using Common Lisp and WebSocket technology | 1,566 |
cpitclaudel/alectryon | A tool for processing Coq and Lean 4 code embedded in text documents | 237 |
xavierleroy/cdf-mech-sem | Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |
abstractsdk/abstract | A modular framework for building secure, composable, and interoperable on-chain applications | 63 |