Zajednički Seminar za matematičku logiku i za teorijsko računarstvo
5 views
Skip to first unread message
Robert Manger
Mar 11, 2020, 8:58:02 AM3/11/20
to seminar-za-teori...@googlegroups.com, vko...@efzg.hr
Dragi kolege,
Na zajedničkom sastanku Seminara za matematičku logiku i Seminara za teorijsko računarstvo, u ponedjeljak 16. ožujka 2020. u 17 sati, u predavaonici 105, PMF-MO, 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.
Predavanje se može pratiti i on-line na sljedećoj adresi: https://meduza.carnet.hr/index.php/media/watch/11640.
Molim sve članove Seminara za teorijsko računarstvo da prisustvuju ovom predavanju.
Lijep pozdrav, Robert Manger.
Na zajedničkom sastanku Seminara za matematičku logiku i Seminara za teorijsko računarstvo, u ponedjeljak 16. ožujka 2020. u 17 sati, u predavaonici 105, PMF-MO, 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.
Predavanje se može pratiti i on-line na sljedećoj adresi: https://meduza.carnet.hr/index.php/media/watch/11640.
Molim sve članove Seminara za teorijsko računarstvo da prisustvuju ovom predavanju.
Lijep pozdrav, Robert Manger.
Reply all
Reply to author
Forward
0 new messages