Language mixing functional programming and Ambient Calculus
-
Updated
May 28, 2024
Language mixing functional programming and Ambient Calculus
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Agda is a dependently typed programming language / interactive theorem prover.
A purely functional programming language with first class types
A Proof-oriented Programming Language
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
A function definition package for Coq
Minimal core language based on dependent function type, pair type, recursive type, sum type and record type.
Dependently-typed range-checked numbers for Scala
The Agda Universal Algebra Library (html docs available at the url below)
Cicada Language (PLCT little team)
Proof assistant based on the λΠ-calculus modulo rewriting
A next-gen functional language
The Higher ORder INtermediate representation - next gen
Cicada Language (solo version)
Accelerated machine learning with dependent types
A work-in-progress core language for Agda, in Agda
Contextual types meet mechanized metatheory!
Universal Data design and transform language core
Add a description, image, and links to the dependent-types topic page so that developers can more easily learn about it.
To associate your repository with the dependent-types topic, visit your repo's landing page and select "manage topics."