All Projects → cicada-lang → cicada

cicada-lang / cicada

Licence: GPL-3.0 license
Cicada Language

Programming Languages

typescript
32286 projects

Projects that are alternatives of or similar to cicada

anders
🧊 Модальний Гомотопічний Прувер
Stars: ✭ 5 (-44.44%)
Mutual labels:  type-system, theorem-prover
Kind
A modern proof language
Stars: ✭ 2,075 (+22955.56%)
Mutual labels:  type-theory, theorem-prover
Isabelle-HoTT
An experimental implementation of homotopy type theory in the interactive proof assistant Isabelle
Stars: ✭ 30 (+233.33%)
Mutual labels:  type-theory, interactive-theorem-proving
pyprover
Resolution theorem proving for predicate logic in pure Python.
Stars: ✭ 71 (+688.89%)
Mutual labels:  prover, theorem-prover
Write You A Haskell
Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)
Stars: ✭ 3,064 (+33944.44%)
Mutual labels:  type-theory, type-system
awesome-rust-formalized-reasoning
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
Stars: ✭ 185 (+1955.56%)
Mutual labels:  prover, theorem-prover
type-operators-rs
A macro for defining type operators in Rust.
Stars: ✭ 56 (+522.22%)
Mutual labels:  type-system
klipse-repl
Beginners friendly Clojure REPL
Stars: ✭ 44 (+388.89%)
Mutual labels:  repl
pyhstr
hstr, but for Python shells
Stars: ✭ 12 (+33.33%)
Mutual labels:  repl
TypeTopology
Logical manifestations of topological concepts, and other things. This version adopts the univalent point of view.
Stars: ✭ 132 (+1366.67%)
Mutual labels:  type-theory
composer-repl
A REPL for PHP built into Composer (using PsySH)
Stars: ✭ 81 (+800%)
Mutual labels:  repl
klisp
A Lisp written in about 200 lines of Ink, featuring an interactive literate programming notebook
Stars: ✭ 28 (+211.11%)
Mutual labels:  repl
openrepl
OpenRepl REPL
Stars: ✭ 27 (+200%)
Mutual labels:  repl
appium-java-repl
Simple Java REPL for controlling mobile apps through Appium.
Stars: ✭ 20 (+122.22%)
Mutual labels:  repl
ostrich
An SMT Solver for string constraints
Stars: ✭ 18 (+100%)
Mutual labels:  theorem-prover
cljs-browser-repl
A ClojureScript REPL and tutorial in your browser!
Stars: ✭ 35 (+288.89%)
Mutual labels:  repl
d3-fdg-svelte
d3 Force Directed Graph example (d3-force) implemented in sveltejs. REPL:
Stars: ✭ 31 (+244.44%)
Mutual labels:  repl
psysh.el
PsySH on Emacs, PHP interactive shell (REPL)
Stars: ✭ 27 (+200%)
Mutual labels:  repl
minitox
Minimal client for Tox
Stars: ✭ 65 (+622.22%)
Mutual labels:  repl
WangsAlgorithm
A classical propositional theorem prover in Haskell, using Wang's Algorithm.
Stars: ✭ 34 (+277.78%)
Mutual labels:  theorem-prover

Cicada Language

[ HOMEPAGE | MANUAL | ABOUT ]

Welcome *^-^*/

Cicada language is a dependently typed programming language and an interactive theorem prover.

The aim of cicada project is to help people understand that developing software and developing mathematics are increasingly the same kind of activity, and people who practice these developments can learn from each other, and help each other in very good ways.

Development

npm install           # Install dependencies
npm run build         # Compile `src/` to `lib/`
npm run build:watch   # Watch the compilation
npm run format        # Format the code
npm run test          # Run test
npm run test:watch    # Watch the testing

Community

GitHub:

Telegram:

Thanks

Thanks PLCT Lab, for sponsoring our community at very early stage of our project.

Thanks Dan Friedman, for we learned most of our knowledge about programming language design from your little books.

Thanks David Christiansen, for coauthoring "The Little Typer" with Dan, and writing up great tutorials (1, 2) about dependent types.

Contributions

Be polite. Do NOT bring negative emotion to others.

To make a contribution, fork this project and create a pull request.

Please read the STYLE-GUIDE.md before you change the code.

Remember to add yourself to AUTHORS. Your line belongs to you, you can write a little introduction to yourself but not too long.

It is assumed that all non draft PRs are ready to be merged. If your PR is not ready to be merged yet, please make it a draft PR:

During the development of your PR, you can make use of the TODO.md file to record ideas temporarily, and this file should be clean again at the end of your development.

License

GPLv3

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].