Introduction

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.
#
Source Code
Source code of this manual is available at the docs/manual/ directory of cicada repository.
Welcame to give feedback :)
#
Manual as Standard Library
This manual also serve as as the standard library of cicada language.
Example usage:
#
References
#
The Little Typer
I learned about how to implement type system from Dan's little books.
My design of cicada language can be viewed as an exercise after "The Little Typer".
  • Thanks, Daniel P. Friedman (1944 -), and David Thrane Christiansen, for your great dialogs and teachings.
#
Vladimir Voevodsky's talk
I recommend a talk of Vladimir Voevodsky:
It summarises the motivation behind cicada project beautifully.
  • Thanks, Vladimir Voevodsky (1966 - 2017)
Installation
Built-in Types