Učitavanje video playera...
01:03:53
Vedran Čačić: 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.
Objavljeno: 13.05.2020
Unutar kategorije: Obrazovanje

Srodni zapisi