Stars
A proof checker meant for education. Primarily for teaching proofs of correctness of functional programs.
The Plutus language implementation and tools
Mirror of the Glasgow Haskell Compiler. Please submit issues and patches to GHC's Gitlab instance (https://gitlab.haskell.org/ghc/ghc). First time contributors are encouraged to get started with th…
A cost-aware logical framework, embedded in Agda.
Multi-engine SMT-based automatic model checker for safety properties of Lustre programs
Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
Spotify song downloader without injecting into the windows client
A work-in-progress core language for Agda, in Agda
Haskell to VHDL/Verilog/SystemVerilog compiler
High level commands to declare a hierarchy based on packed classes
Documentation and tools relating to the design and prototyping of Ouroboros Leios
A purely functional programming language with first class types
Framework for generating constrained random data using a subset of first order logic
Logical manifestations of topological concepts, and other things, via the univalent point of view.
A collection of formalized statements of conjectures in Lean.
This repository hosts the lectures of the Plutus Pioneers Program. This program is a training course that the IOG Education Team provides to recruit and train software developers in Plutus, the nat…
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…
An agda2hs-compatible library for well-scoped syntax
A toolkit for enforcing logical specifications on neural networks
A libre lightweight streaming front-end for Android.
Formally Verified Arguments of Knowledge in Lean
Mathematical terms, definitions, and propositions in as many languages as possible