Subjects

Your browser does not support JavaScript, or its support is disabled. Some features may not be available.

Formalization seminar - NMAG585

Title:	Formalizační seminář
Guaranteed by:	Department of Algebra (32-KA)
Faculty:	Faculty of Mathematics and Physics
Actual:	from 2023
Semester:	winter
E-Credits:	2
Hours per week, examination:	winter s.:0/2, C [HT]
Capacity:	unlimited
Min. number of students:	unlimited
4EU+:	no
Virtual mobility / capacity:	no
State of the course:	taught
Language:	Czech
Teaching methods:	full-time
Teaching methods:	full-time
Additional information:	http://www.karlin.mff.cuni.cz/~holub/formalizace.htm
Note:	you can enroll for the course repeatedly

Guarantor:	doc. Mgr. Štěpán Holub, Ph.D.

Opinion survey results Examination dates WS schedule Noticeboard

Annotation -

Last update: doc. Mgr. Štěpán Holub, Ph.D. (25.08.2023)

Seminar is intended for those interested in interactive proof systems that allow formal verification of mathematical proofs. The content of the seminar is a hands on introduction to the Isabelle/HOL proof assistant at the user level allowing the formalization of specific selected topics.

Course completion requirements -

Last update: doc. Mgr. Štěpán Holub, Ph.D. (25.08.2023)

Active participation and formalization of a selected material is required.

Literature - Czech

Last update: doc. Mgr. Štěpán Holub, Ph.D. (25.08.2023)

Isabelle proof assistant. https://isabelle.in.tum.de/

Archive of formal proofs. https://www.isa-afp.org/