pi/README.md

# pi

A dependently typed system

# Implemented

* A Basic dependent lambda calculus
  * lambda abstractions
  * variables
  * pi types
  * type of types

* Unit type

* Empty type

* Natural numbers

* Σ Types

# TODO

* Let ... in ...

* Fun types
  * Id

* Parser

* Implicit arguments

* Universes

* (indexed) inductive datatypes

* Write down the rules (I'll not get this far)

# References

Some of the material I found helpful in groking dependent type checking:

* Coquand, Thierry. “An Algorithm for Type-Checking Dependent Types.” Science of Computer Programming 26, no. 1–3 (May 1996): 167–77. https://doi.org/10.1016/0167-6423(95)00021-6.

* Brady, Edwin. "SPLV20 course notes". GitHub. https://github.com/edwinb/SPLV20
-												add readme

											
										
										
											2022-05-16 17:40:01 +02:00
+								# pi
-												implemented types ⊤, ⊥, and ℕ

											
										
										
											2022-07-21 00:05:45 +02:00
-												add readme

											
										
										
											2022-05-16 17:40:01 +02:00
+								A dependently typed system
-												implemented types ⊤, ⊥, and ℕ

											
										
										
											2022-07-21 00:05:45 +02:00
+								# Implemented
 								* A Basic dependent lambda calculus
 								  * lambda abstractions
 								  * variables
 								  * pi types
 								  * type of types
 								* Unit type
 								* Empty type
 								* Natural numbers
-												added Σ types to readme also

											
										
										
											2022-07-21 04:20:20 +02:00
+								* Σ Types
-												add readme

											
										
										
											2022-05-16 17:40:01 +02:00
+								# TODO
-												added let in to TODO

											
										
										
											2022-07-21 04:19:47 +02:00
+								* Let ... in ...
-												implemented types ⊤, ⊥, and ℕ

											
										
										
											2022-07-21 00:05:45 +02:00
+								* Fun types
-												updated plan

											
										
										
											2022-07-20 21:22:35 +02:00
+								  * Id
-												add readme

											
										
										
											2022-05-16 17:40:01 +02:00
-												implemented types ⊤, ⊥, and ℕ

											
										
										
											2022-07-21 00:05:45 +02:00
+								* Parser
-												updated plan

											
										
										
											2022-07-20 21:22:35 +02:00
+								* Implicit arguments
-												add readme

											
										
										
											2022-05-16 17:40:01 +02:00
-												updated plan

											
										
										
											2022-07-20 21:22:35 +02:00
+								* Universes
-												add some references to useful material in the readme

											
										
										
											2022-05-16 17:49:56 +02:00
-												implemented types ⊤, ⊥, and ℕ

											
										
										
											2022-07-21 00:05:45 +02:00
+								* (indexed) inductive datatypes
 								* Write down the rules (I'll not get this far)
-												add some references to useful material in the readme

											
										
										
											2022-05-16 17:49:56 +02:00
+								# References
 								Some of the material I found helpful in groking dependent type checking:
 								* Coquand, Thierry. “An Algorithm for Type-Checking Dependent Types.” Science of Computer Programming 26, no. 1–3 (May 1996): 167–77. https://doi.org/10.1016/0167-6423(95)00021-6.
 								* Brady, Edwin. "SPLV20 course notes". GitHub. https://github.com/edwinb/SPLV20