Tez No	İndirme	Tez Künye	Durumu
540537		Verification of sequencel programs using Mizar / Yazar:ADEM ÖZYAVAŞ Danışman: Dr. NELSON J. RUSTHON Yer Bilgisi: Texas Tech University / Yurtdışı Enstitü Konu:Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol = Computer Engineering and Computer Science and Control Dizin:	Onaylandı Doktora İngilizce 2010 79 s.
Purely functional language programs are claimed to lend themselves more easily to their proof of correctness. SequenceL, exclusively designed at Texas Tech University, is a strict functional language. There are some proof-assistants used in verification of functional language programs. In this research, we used one of the available proof assistants called Mizar to prove correctness of SequenceL programs. Mizar is based on Tarski-Grothendieck set theory formulated in a first-order language. The Mizar language is human readable compared to other formal systems. It also has some other desirable features for our purposes. The result of this research is a Mizar file that describes a semantics of SequenceL and the framework in which properties of SequenceL programs can be proved. Some examples such as factorial and Euclidian greatest common divisor are given in the Mizar file. Also, a reasonably sized library of proven statements is provided intended to shorten the proofs of properties of SequenceL programs.