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: 5 months ago coqsyntaxvariable-binding
Related projects:
Repository | Description | Stars |
---|---|---|
| A tool for generating Coq code from syntactic theories with variable binders | 17 |
| A flexible data model and API for representing linguistic data in a language-independent and theory-neutral way. | 15 |
| A Coq library providing structural tactics and utility definitions to simplify proof development in proof assistants. | 21 |
| A framework for implementing and verifying distributed systems using Coq | 95 |
| A comprehensive survey of programming language semantics styles implemented in Coq | 46 |
| A foundational framework for modular cryptographic proofs in Coq | 56 |
| Provides encapsulation of domain logic and business rules in an application layer using the Command pattern and source generator. | 59 |
| A tool for interactive theorem proving and language support in Coq | 153 |
| Formalizations of functional languages with a focus on proof and verification | 142 |
| A Coq-based library providing a formal verification framework for the Tezos smart contract language | 28 |
| An implementation of System F in Coq, aiming to provide a rigorous and expressive formal system for describing programming languages. | 19 |
| A GUI framework that enables web-based graphical user interfaces using Common Lisp and WebSocket technology | 1,566 |
| A tool for processing Coq and Lean 4 code embedded in text documents | 237 |
| Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |
| A modular framework for building secure, composable, and interoperable on-chain applications | 63 |