HOL-Theorem-Prover / Hol
Licence: other
Canonical sources for HOL4 theorem-proving system. Branch `develop` is where “mainline development” occurs; when `develop` passes our regression tests, `master` is merged forward to catch up.
Stars: ✭ 414
Labels
Projects that are alternatives of or similar to Hol
Cedille
Cedille, a dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations
Stars: ✭ 289 (-30.19%)
Mutual labels: lambda-calculus
vanilla-lang
An implementation of a predicative polymorphic language with bidirectional type inference and algebraic data types
Stars: ✭ 73 (-82.37%)
Mutual labels: lambda-calculus
Krivine-Machine
Abstract krivine machine implementing call-by-name semantics. In OCaml.
Stars: ✭ 34 (-91.79%)
Mutual labels: lambda-calculus
ATS-blockchain
⛓️ Blockchain + Smart contracts from scratch
Stars: ✭ 18 (-95.65%)
Mutual labels: lambda-calculus
meta-cedille
Minimalistic dependent type theory with syntactic metaprogramming
Stars: ✭ 40 (-90.34%)
Mutual labels: lambda-calculus
lambda-fibonacci
Implementation of the Fibonacci sequence in JS using pure Lambda Calculus
Stars: ✭ 18 (-95.65%)
Mutual labels: lambda-calculus
Write You A Haskell
Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)
Stars: ✭ 3,064 (+640.1%)
Mutual labels: lambda-calculus
LambdaCalculusPlayground
An Android app that provides a visual interface for creating and evaluating lambda calculus expressions
Stars: ✭ 16 (-96.14%)
Mutual labels: lambda-calculus
salt
The compilation target that functional programmers always wanted.
Stars: ✭ 62 (-85.02%)
Mutual labels: lambda-calculus
types-and-programming-languages
Exercises from Benjamin Pierce's "Types and Programming Languages" textbook + extras!
Stars: ✭ 92 (-77.78%)
Mutual labels: lambda-calculus
lambda-calculus
An introduction to the Lambda Calculus
Stars: ✭ 59 (-85.75%)
Mutual labels: lambda-calculus
Lambda
🔮 Estudos obscuros de programação funcional
Stars: ✭ 297 (-28.26%)
Mutual labels: lambda-calculus
system-F
Formalization of the polymorphic lambda calculus and its parametricity theorem
Stars: ✭ 20 (-95.17%)
Mutual labels: lambda-calculus
Type-Theory
Lecture note on Lambda Calculus and Types for FLOLAC
Stars: ✭ 26 (-93.72%)
Mutual labels: lambda-calculus
Plam
An interpreter for learning and exploring pure λ-calculus
Stars: ✭ 385 (-7%)
Mutual labels: lambda-calculus
Lambda Talk
A Flock of Functions: Combinators, Lambda Calculus, & Church Encodings in JS
Stars: ✭ 315 (-23.91%)
Mutual labels: lambda-calculus
lplzoo
Fine-grain implementations of common lambda calculi in Haskell, tested with QuickCheck
Stars: ✭ 32 (-92.27%)
Mutual labels: lambda-calculus
This is the distribution directory for the Kananaskis release of HOL4. See http://hol-theorem-prover.org for online resources.
The following is a brief listing of what's available in the distribution.
INSTALL * Installation instructions
COPYRIGHT * Copyright notice
std.prelude * File loaded at the beginning of each HOL session
bin/ * Executables
doc/ * Some documentation, including release notes
examples/ * Some examples
help/ * Help support
src/ * The system sources
tools/ * Support for building the system
sigobj/ * Collection of all signatures and compiled code
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].