mortberg / cubicaltt

Experimental implementation of Cubical Type Theory
https://arxiv.org/abs/1611.02108
MIT License
571 stars 76 forks source link

Learning Guide #57

Closed ronaldpetty closed 7 years ago

ronaldpetty commented 7 years ago

Hello,

I am totally new to this area. I would be interested in the following.

Totally not trying to belittle, just really like to try to understand.

Thank you!

mortberg commented 7 years ago

I've given a series of lectures on cubicaltt recently, the notes can be found at: https://github.com/mortberg/cubicaltt/tree/master/lectures

These notes assume a lot more than you are asking for, but as this is a very experimental research project under development I don't think we can provide such a detailed list of background topics. If you are interested in formal verification of software and mathematics I suggest you start by looking at mature systems like Coq or Agda. There are a lot of very good books and tutorials on these systems out there, for instance https://softwarefoundations.cis.upenn.edu/current/index.html.

ronaldpetty commented 7 years ago

Awesome!