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
- 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
- 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
- Effect of circular and slot jet impingement design on anti-icing system of an aircraft wing leading edge
Bir uçağın kanat hücum kenarının buz çözme sistemi üzerinde dairesel ve slot jet çarpma tasarımının etkisi
HAYATİ KADİR PAZARLIOĞLU
Yüksek Lisans
İngilizce
2022
Makine MühendisliğiKarabük ÜniversitesiMakine Mühendisliği Ana Bilim Dalı
PROF. DR. KAMİL ARSLAN
DR. ÖĞR. ÜYESİ AHMET ÜMİT TEPE
- Association rule mining for identifying factors in dynamic positioning incidents and accidents
Dinamik konumlandırma kazalarına ait faktörlerin birliktelik kural madenciliği ile tanımlanması
TUĞFAN ŞAHİN
Doktora
İngilizce
2024
Deniz Bilimleriİstanbul Teknik ÜniversitesiDeniz Ulaştırma Mühendisliği Ana Bilim Dalı
DOÇ. DR. PELİN BOLAT