Tipi v programskih jezikih in izreki o varnosti programov - Koprivec, Filip (Obzornik za matematiko in fiziko, 2017)
One of the most important tools in programming is definitely the type system, which allows us to eliminate a whole class of errors before the actual evaluation od the program even takes place. The article presents a simple programming language which is used to examine syntax and evaluation rules, and proceeds with proving a safety theorem which uses types to ensure that the program state will stay sound during the execution. Simply type lambda calculus and the corresponding safety theorem are presented at the end.
Keywords: izreki o varnosti; izvajanje; programski jezik; sintaksa; tipi