Walter Schulze
@awalterschulze.bsky.social
PhD Informatics Student
As a thank you for 1000 views of our talk: Correct Code by Construction by @paulcadman.dev and I. We have decided to write up the talk in a blog post: A taste of Coq betterprogramming.pub/a-taste-of-c... for those who prefer to consume it in a different format.
https://medium.com/bette…
December 18, 2024 at 9:55 AM
As a thank you for 1000 views of our talk: Correct Code by Construction by @paulcadman.dev and I. We have decided to write up the talk in a blog post: A taste of Coq betterprogramming.pub/a-taste-of-c... for those who prefer to consume it in a different format.
All things being equal, Homotopy Type Theory has less equalities between equalities.
Given (x y: a = b) you can prove x = y, because of UIP (Uniqueness of Identity Proofs) which says there is only one unique way to construct a = b.
Homotopy Type Theory does not have UIP, so ...
Given (x y: a = b) you can prove x = y, because of UIP (Uniqueness of Identity Proofs) which says there is only one unique way to construct a = b.
Homotopy Type Theory does not have UIP, so ...
December 6, 2024 at 3:13 PM
All things being equal, Homotopy Type Theory has less equalities between equalities.
Given (x y: a = b) you can prove x = y, because of UIP (Uniqueness of Identity Proofs) which says there is only one unique way to construct a = b.
Homotopy Type Theory does not have UIP, so ...
Given (x y: a = b) you can prove x = y, because of UIP (Uniqueness of Identity Proofs) which says there is only one unique way to construct a = b.
Homotopy Type Theory does not have UIP, so ...
I have been fiscally responsible, but now it is time to be physically responsible and get phd.
December 2, 2024 at 3:09 PM
I have been fiscally responsible, but now it is time to be physically responsible and get phd.