cedille / Cedille
Licence: other
Cedille, a dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations
Stars: ✭ 289
Labels
Projects that are alternatives of or similar to Cedille
lambda-notebook
Lambda Notebook: Formal Semantics in Jupyter
Stars: ✭ 16 (-94.46%)
Mutual labels: lambda-calculus
LambdaCalculusPlayground
An Android app that provides a visual interface for creating and evaluating lambda calculus expressions
Stars: ✭ 16 (-94.46%)
Mutual labels: lambda-calculus
Type-Theory
Lecture note on Lambda Calculus and Types for FLOLAC
Stars: ✭ 26 (-91%)
Mutual labels: lambda-calculus
universe-of-syntax
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.
Stars: ✭ 16 (-94.46%)
Mutual labels: lambda-calculus
lambda-calculus
An introduction to the Lambda Calculus
Stars: ✭ 59 (-79.58%)
Mutual labels: lambda-calculus
salt
The compilation target that functional programmers always wanted.
Stars: ✭ 62 (-78.55%)
Mutual labels: lambda-calculus
gidti
Book: Gentle Introduction to Dependent Types with Idris
Stars: ✭ 70 (-75.78%)
Mutual labels: lambda-calculus
lplzoo
Fine-grain implementations of common lambda calculi in Haskell, tested with QuickCheck
Stars: ✭ 32 (-88.93%)
Mutual labels: lambda-calculus
vanilla-lang
An implementation of a predicative polymorphic language with bidirectional type inference and algebraic data types
Stars: ✭ 73 (-74.74%)
Mutual labels: lambda-calculus
meta-cedille
Minimalistic dependent type theory with syntactic metaprogramming
Stars: ✭ 40 (-86.16%)
Mutual labels: lambda-calculus
Krivine-Machine
Abstract krivine machine implementing call-by-name semantics. In OCaml.
Stars: ✭ 34 (-88.24%)
Mutual labels: lambda-calculus
pomagma
An inference engine for extensional untyped λ-calculus
Stars: ✭ 15 (-94.81%)
Mutual labels: lambda-calculus
ATS-blockchain
⛓️ Blockchain + Smart contracts from scratch
Stars: ✭ 18 (-93.77%)
Mutual labels: lambda-calculus
abella
An interactive theorem prover based on lambda-tree syntax
Stars: ✭ 81 (-71.97%)
Mutual labels: lambda-calculus
Write You A Haskell
Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)
Stars: ✭ 3,064 (+960.21%)
Mutual labels: lambda-calculus
types-and-programming-languages
Exercises from Benjamin Pierce's "Types and Programming Languages" textbook + extras!
Stars: ✭ 92 (-68.17%)
Mutual labels: lambda-calculus
lambda-fibonacci
Implementation of the Fibonacci sequence in JS using pure Lambda Calculus
Stars: ✭ 18 (-93.77%)
Mutual labels: lambda-calculus
The Cedille Programming Language
Please see the Cedille homepage for an introduction to Cedille.
Repository Content Highlights
-
cedille-mode/: Elisp code for the Cedille Emacs mode -
cedille-tests/: Unit tests for the Cedille Emacs frontend -
core/: A Haskell implementation of a Cedille Core checker -
language-overview/: Example Cedille programs that demonstrate some of its important features -
lib/: The (provisional) Cedille Standard Library -
parser/: The parser for the Cedille language (written in Haskell) -
se-mode/: The Elisp source code for the Emacs "Structured Editing Mode" -
src/: The Cedille source code (written in Agda)
License
MIT
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].