Skip to content
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
CNAME
README.md
cafe.pdf
cafe.sketch

README.md

HoTT: The Language of Space

Groupoid Infinity Presentation (Slides) for Public Event f(cafe) 25 July 2018 https://www.facebook.com/kievfprog/posts/1626535840802381
DOI: 10.13140/RG.2.2.36617.34402

Abstract

Homotopy Type Theory (HoTT) is the most advanced programming language in the domain of intersection of several theories: algebraic topology, homological algebra, higher category theory, mathematical logic, and theoretical computer science. That is why it can be considered as a language of space, as it can encode any existent mathematics.

Speaker: Maxim Sokhatsky is an author of Privat24 deposits, 20 years of working experience as a programmer, one of the 30 top-commiters in Ukraine in Open Source, author of N2O, the best Erlang Web Framework, CEO of Synrc Research Center, author of several embedded operating system runtimes and production programming languages. Maxim is familiar with any programming language on the planet and had seen sources of all operating systems.

Now Maxim is doing his Ph.D. research (the second year of education) in HoTT, trying to encode as much mathematics in the programming language as possible along the way.

During this lecture, Maxim will try to smoothly guide you from the programming perspective to the pure space of mathematics and will show the evolution of mathematical provers from AUTOMATH to the family of Cubical Type Checkers. Also, this lecture is considered as a general introduction to HoTT course Maxim is preparing for his friends.

Credits

You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.