76 Open source projects that are alternatives of or similar to pomagma

Book: Gentle Introduction to Dependent Types with Idris

implementation of Pure Type Systems (PTS) in Rust.

Lecture note on Lambda Calculus and Types for FLOLAC

An introduction to the Lambda Calculus

Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)

An implementation of the Formality language in JavaScript

The compilation target that functional programmers always wanted.

Resolution theorem proving for predicate logic in pure Python.

Some incremental examples suitable to host an AWS Lambda Functions workshop

A universe of scope- and type-safe syntaxes (syntices?). Includes generic implementation of type-preserving renaming/substitution with all the proofs you could possibly need.

Coq encoding of ZFC and formalization of the textbook Elements of Set Theory

🔮 Estudos obscuros de programação funcional

🍱 Y Combinator for Non-programmers: A Wild Introduction to Computer Science

Exercises from Benjamin Pierce's "Types and Programming Languages" textbook + extras!

A Machine Learning System for Data Enrichment.

Implementation of the Fibonacci sequence in JS using pure Lambda Calculus

(λ) Educational lambda calculus interpreter

An Android app that provides a visual interface for creating and evaluating lambda calculus expressions

A minimalist pure lazy functional programming language

Formalization of the polymorphic lambda calculus and its parametricity theorem

A statically-typed strictly-evaluated garbage-collected readable programming language.

Homepage Theorem Proving in Lean FAQ

Elsa is a lambda calculus evaluator

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.

No description or website provided.

Jupyter kernel for Coq

A Flock of Functions: Combinators, Lambda Calculus, & Church Encodings in JS

🐦 Some combinators

Cedille, a dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations

Bologna Optimal Higher-Order Machine, Version 1.1

Fine-grain implementations of common lambda calculi in Haskell, tested with QuickCheck

⛪️ Church Encoding in JS

⛓️ Blockchain + Smart contracts from scratch

Powerful Light Artificial NEuRon inference framework for CNN

Lambda calculus go brrrr

Fun with λ calculus!

Abstract krivine machine implementing call-by-name semantics. In OCaml.

Efficient and single-steppable ULC evaluation algorithm

lambda calculus interpreter

A simple, zero-dependency implementation of the untyped lambda calculus in Safe Rust

An implementation of a predicative polymorphic language with bidirectional type inference and algebraic data types

An interactive theorem prover based on lambda-tree syntax

Macro Lambda Calculus

λtext - higher-order file applicator

Minimalistic dependent type theory with syntactic metaprogramming

Automatic code generation for Scala functions and expressions via the Curry-Howard isomorphism

A Proof-oriented Programming Language

Formalisation of the linear lambda calculus in Coq

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.

Razor is a tool for constructing finite models for first-order theories

LinearOne is a prototype theorem prover for first-order (multiplicative, intuitionistic) linear logic.

A library for functional programming in Rust

A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.

A modern proof language

Lambda Notebook: Formal Semantics in Jupyter

An interpreter for learning and exploring pure λ-calculus

Public code developed during my MSc study at University of Bologna

Church Encoding Implementation in JavaScript

Coq formalizations of functional languages.

十分钟魔法练习