Predmetni nastavnik prof. Silvia Gilezan
Predmetni asistent Marina Kalaba, Simona Prokić
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:
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
Slajdovi, beleške i predavanja:
OPLSS 2023 - Oregon Programming Languages Summer School
OPLSS 2025 - Oregon Programming Languages Summer School
Linkovi:
Masive Open Online Course (MOOC): Coursera
MIT OpenCourseWare
ArXiv - open access articles
LaTeX