Seminar za matematičku logiku i osnove matematike
lokacija:
PMF Matematički odsjek (virtualno)
vrijeme:
11.05.2020 - 17:00 - 19:00 Na Seminaru za matematičku logiku i osnove matematike, u ponedjeljak 11. svibnja 2020. u 17 sati,
Vedran Čačić će održati predavanje
Calculus of inductive constructions
Sažetak: Bit će predstavljen račun induktivnih konstrukcija (CIC), koji predstavlja teorijsku osnovu za dokazivač Coq. CIC je nadogradnja starijeg sustava CoC (Calculus of Constructions, vrsta teorije tipova) induktivnim tipovima koji se shvaćaju kao najmanje fiksne točke određenih kategoroloških "polinoma". Unutar CICa može se razvijati klasična i konstruktivna logika sudova, prvog reda i viših redova, te formalizirati brojne temeljne matematičke discipline kao što je teorija skupova ili homotopska teorija tipova. Može poslužiti i za verifikaciju i ekstrakciju programa u funkcijskim programskim jezicima (a kroz denotacijsku semantiku i u imperativnima). U skladu s Curry-Howardovim izomorfizmom, propozicije se shvaćaju kao tipovi, a dokaz propozicije je term odgovarajućeg tipa.
Seminar će se održati putem Zoom-a.
Link i potrebni podaci su ovdje:
https://zoom.us/j/92305464243?pwd=TjUwa3VyTG5KT0pIbzluUURBemxJdz09
Meeting ID: 923 0546 4243
Password: 020169
Ako nemate klijentski program za Zoom, možete ga besplatno skinuti ovdje:
