Predmetni nastavnik prof. Silvia Gilezan
Predmetni asistent Simona Prokić
Literatura:
Interaktivni dokazivači:
The COQ Proof Assistant
Isabelle, generic proof assistant
AGDA, proof assistant and dependently typed functional programming language
Henk Barendregt: Lambda Calculus with Types
Lawrence Paulson: Isabelle - A Generic Theorem Prover, Springer
Benjamin Pierce: Software Foundations
Filip Maric: A Survey of Interactive Theorem Proving
Linkovi:
Masive Open Online Course (MOOC): Coursera
MIT OpenCourseWare
ArXiv - open access articles
LaTeX
Način provere znanja:
- Pismeni deo ispita: zadaci i teorija (50)
- Seminarski rad, tema po dogovoru (30)
- Usmena odbrana seminarskog rada (20)