Uvod u funkcionalne programske jezike
Predmet je namenjen studentima doktorskih studija Fakulteta tehničkih nauka u Novom Sadu.
Predmetni nastavnik prof. Silvia Gilezan
Interaktivni dokazivači:
ROCQ Prover (formerly COQ Proof Assistant)
Isabelle, generic proof assistant
AGDA, proof assistant and dependently typed functional programming language
LEAN, theorem prover (proof assistant) and functional programming language
Literatura:
Lawrence Paulson: Isabelle - A Generic Theorem Prover, Springer
Benjamin Pierce: Software Foundations
Filip Maric: A Survey of Interactive Theorem Proving
Dodatna literatura i informacije su dostupni na stranici predmeta Logika u računarstvu