Cześć Mirki. Ostatnio zacząłem na pewnym kole naukowym na pewnej polskiej uczelni prowadzić zajęcia z języka Coq i chciałbym się podzielić z wami tworzonymi przeze mnie materiałami dydaktycznymi: zeimer.github.io
Czym jest Coq? Jest to asystent dowodzenia twierdzeń oraz język programowania oparty na teorii typów. Umożliwia nam programowanie funkcyjne (jak w Haskellu, tylko na sterydach) oraz "robienie matematyki" (definiowanie obiektów matematycznych, dowodzenie ich właściwości etc.). Jest warty uwagi, bo dzięki temu
























Scalowa confa w Gdańsku, stream live:
https://gaming.youtube.com/channel/UC1VAdzkoY7M2e3msbW9Ur8w/live