Groupoid Infinity Presentation (Slides) for Public Event, Kyiv, Ukraine, f(cafe), 25 July 2018 DOI: 10.13140/RG.2.2.36617.34402 cafe.groupoid.space/cafe.pdf
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.
Groupoid Infinity Presentation (Slides) for Public Event Quanterall HQ Varna, Bulgaria, 13 June 2019
DOI: 10.13140/RG.2.2.28584.21763 cafe.groupoid.space/languages.pdf
Introduction to Formal Languages, its Design and Implementations. Three practial modern pure languages will be disclosed: Plutus (Haskell), Morte (Erlang), Formality (Rust).
Voxoz Presentation (Slides) for Public Event Quanterall HQ Varna, Bulgaria, 27 June 2019
DOI: 10.13140/RG.2.2.28584.21763 cafe.groupoid.space/systems.pdf
Introduction to Operating Systems, its Design and Implementations. POSIX, Microkernels, Unikernels. Real time unikernel with O vector processing language will be disclosed.
Public Event, Kyiv, Ukraine, Groupoid Cafe, 17 July 2021
DOI: 10.13140/RG.2.2.25096.55040 cafe.groupoid.space/anders.0.7.2.pdf
The HTS language proposed by Voevodsky exposes two different presheaf models of type theory: the inner one is homotopy type system presheaf that models HoTT and the outer one is traditional Martin-Löf type system presheaf that models set theory with UIP. The motivation behind this doubling is to have an ability to express semisemplicial types. Theoretical work on merging inner and outer languages was continued in 2LTT.
While we are on our road to Lean-like tactic language, currently
we are at the stage of regular cubical HTS type checker with CHM-style
primitives. You may try it at Github:
groupoid/anders or
install with opam: opam install anders.