Certi cations of programs with computational effects
Başlık çevirisi mevcut değil.
- Tez No: 403359
- Danışmanlar: Dr. JEAN- GUILLAUME DUMAS, Dr. DOMINIQUE DUVAL
- Tez Türü: Doktora
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
- Anahtar Kelimeler: computational effects, states, exceptions, program property proofs, equational semantics, decorated logic, proof certification, Coq
- Yıl: 2016
- Dil: İngilizce
- Üniversite: Université Grenoble Alpes
- Enstitü: Yurtdışı Enstitü
- Ana Bilim Dalı: Belirtilmemiş.
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 160
Özet
Özet yok.
Özet (Çeviri)
In this thesis, we aim to formalize the effects of a computation. Indeed, most used programming languages involve different sorts of effects: state change, exceptions, input/ output, non-determinism, etc. They may bring ease and flexibility to the coding process. However, the problem is to take into account the effects when proving the properties of programs. The major difficulty in such kind of reasoning is the mismatch between the syntax of operations with effects and their interpretation. Typically, a piece of program with arguments in X that returns a value in Y is not interpreted as a function from X to Y, due to the effects. The best-known algebraic approach to the problem interprets programs including effects with the use of monads: the interpretation is a function from X to T(Y) where T is a monad. This approach has been extended to Lawvere theories and algebraic handlers. Another approach called, the decorated logic, provides a sort of equational semantics for reasoning about programs with effects. We specialize the approach of decorated logic to the state and the exceptions effects by defining the decorated logic for states (Lst) and the decorated logic for exceptions (Lexc), respectively. This enables us to prove properties of programs involving such effects. Then, we formalize these logics in Coq and certify the related proofs. These logics are built so as to be sound. In addition, we introduce a relative notion of syntactic completeness of a theory in a given logic with respect to a sublogic. We prove that the decorated theory for the global states as well as two decorated theories for exceptions are syntactically complete relatively to their pure sublogics. These proofs are certified in Coq as applications of our generic frameworks.
Benzer Tezler
- Avrupa yeşil mutabakatı çerçevesinde moda endüstrisinin sürdürülebilirlik uyum süreçleri: Türkiye perspektifi
Sustainability compliance processes of the fashion industry within the framework of the European green deal: Policies, programs and future perspective in the context of Turkey
DERYA YILDIZ
Yüksek Lisans
Türkçe
2025
Tekstil ve Tekstil MühendisliğiIşık ÜniversitesiModa ve Tekstil Tasarımı Ana Bilim Dalı
YRD. DOÇ. DR. MELİHA PINAR SİPAHİ
- Sürdürülebilir konut cephelerinin tasarım kriterleri üzerine bir inceleme: İngiltere örneği
An assessment on design criterias of sustainable housing facades: The case of England
PELİN ARSLAN
Yüksek Lisans
Türkçe
2017
Mimarlıkİstanbul Teknik ÜniversitesiMimarlık Ana Bilim Dalı
DOÇ. DR. SEDEN ACUN ÖZGÜNLER
- Sürdürülebilirlik ilkeleri kapsamındaki standart vesertifikasyonların Türkiye mobilya endüstrisine yönelikincelenmesi
Examination of standards and certifications within the scopeof sustainability principles for the furniture industry inTürkiye
YEŞİM YÜZAY BEKTAŞ
Yüksek Lisans
Türkçe
2025
Ağaç İşleriİstanbul Üniversitesi-CerrahpaşaOrman Endüstri Mühendisliği Ana Bilim Dalı
PROF. DR. TUNCER DİLİK
- Gıda üretim zincirinde uygulanan gıda güvenliği yönetimisistemlerinin karşılaştırılması
Compari̇son of food safety management systems implemented i̇n food producti̇on chai̇ns
AYŞE AYTEKİN
Yüksek Lisans
Türkçe
2017
Gıda Mühendisliğiİstanbul Aydın ÜniversitesiGıda Mühendisliği Ana Bilim Dalı
PROF. DR. GÜNER ARKUN
- Yapı bilgi modelleme aracılığı ile enerji etkin yapı tasarımı ve geliştirilmesi: Bir konut projesi örneği
Energy efficient design and enhance of buildings with building information modelling: The case of a multistory residential building
DAMLA ELBİ
Yüksek Lisans
Türkçe
2019
Enerjiİstanbul Teknik ÜniversitesiMimarlık Ana Bilim Dalı
PROF. DR. GÜL KOÇLAR ORAL