All Projects β†’ abella-prover β†’ abella

abella-prover / abella

Licence: GPL-3.0 license
An interactive theorem prover based on lambda-tree syntax

Programming Languages

ocaml
1615 projects
Standard ML
205 projects
emacs lisp
2029 projects
Makefile
30231 projects

Projects that are alternatives of or similar to abella

Zion
A statically-typed strictly-evaluated garbage-collected readable programming language.
Stars: ✭ 33 (-59.26%)
Mutual labels:  lambda-calculus
Y Combinator For Non Programmers
🍱 Y Combinator for Non-programmers: A Wild Introduction to Computer Science
Stars: ✭ 109 (+34.57%)
Mutual labels:  lambda-calculus
StepULC
Efficient and single-steppable ULC evaluation algorithm
Stars: ✭ 15 (-81.48%)
Mutual labels:  lambda-calculus
Pts
implementation of Pure Type Systems (PTS) in Rust.
Stars: ✭ 41 (-49.38%)
Mutual labels:  lambda-calculus
Formality Javascript
An implementation of the Formality language in JavaScript
Stars: ✭ 71 (-12.35%)
Mutual labels:  lambda-calculus
Iron
Coq formalizations of functional languages.
Stars: ✭ 114 (+40.74%)
Mutual labels:  lambda-calculus
Aws Lambda Workshop
Some incremental examples suitable to host an AWS Lambda Functions workshop
Stars: ✭ 18 (-77.78%)
Mutual labels:  lambda-calculus
lambda-zero
A minimalist pure lazy functional programming language
Stars: ✭ 65 (-19.75%)
Mutual labels:  lambda-calculus
Church
β›ͺ️ Church Encoding in JS
Stars: ✭ 107 (+32.1%)
Mutual labels:  lambda-calculus
Curryhoward
Automatic code generation for Scala functions and expressions via the Curry-Howard isomorphism
Stars: ✭ 229 (+182.72%)
Mutual labels:  lambda-calculus
Lambda calculus
A simple, zero-dependency implementation of the untyped lambda calculus in Safe Rust
Stars: ✭ 46 (-43.21%)
Mutual labels:  lambda-calculus
Lambda
Fun with Ξ» calculus!
Stars: ✭ 65 (-19.75%)
Mutual labels:  lambda-calculus
Kind
A modern proof language
Stars: ✭ 2,075 (+2461.73%)
Mutual labels:  lambda-calculus
Ltext
Ξ»text - higher-order file applicator
Stars: ✭ 37 (-54.32%)
Mutual labels:  lambda-calculus
BOHM1.1
Bologna Optimal Higher-Order Machine, Version 1.1
Stars: ✭ 45 (-44.44%)
Mutual labels:  lambda-calculus
Dblib Linear
Formalisation of the linear lambda calculus in Coq
Stars: ✭ 10 (-87.65%)
Mutual labels:  lambda-calculus
Combinators Js
🐦 Some combinators
Stars: ✭ 114 (+40.74%)
Mutual labels:  lambda-calculus
gidti
Book: Gentle Introduction to Dependent Types with Idris
Stars: ✭ 70 (-13.58%)
Mutual labels:  lambda-calculus
js-church-encoding
Church Encoding Implementation in JavaScript
Stars: ✭ 33 (-59.26%)
Mutual labels:  lambda-calculus
Elsa
Elsa is a lambda calculus evaluator
Stars: ✭ 135 (+66.67%)
Mutual labels:  lambda-calculus

Quick Start

Compile Abella by running "make" from the root directory. This will create the binary "abella" (on Unix-like systems, including Mac OS X), or "abella.exe" (on Windows). This binary can be freely copied anywhere.

Use the following walkthrough for an introduction to using Abella:

http://abella-prover.org/walkthrough.html

More Information

More information on Abella is available at

http://abella-prover.org/

Bugs, Feature Requests, and Issues

Please report all bugs, feature requests, and issues on the GitHub issue tracker for Abella, available from:

https://github.com/abella-prover/abella/issues

Discussion of Abella and its uses happens on this mailing list.

http://groups.google.com/group/abella-theorem-prover

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].