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ü: Belirtilmemiş.
- Konular: Belirtilmemiş.
- Anahtar Kelimeler: computational effects, states, exceptions, program property proofs, equational semantics, decorated logic, proof certification, Coq
- Yıl:
- Dil:
- Üniversite: Unıversıte Grenoble Alpes
- Enstitü: Yurtdışı Enstitü
- Ana Bilim Dalı: Belirtilmemiş.
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: Belirtilmemiş.
Ö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
- Farklı elektrotların klor alkali prosesinde hidrojen ve klor gazı üretimine etkisi
Effect of different electrodes on hydrogen and chlorine gas production in chlor alkaliprocess
ZEYNEP CEREN GÜMÜŞ
Yüksek Lisans
Türkçe
2026
Çevre MühendisliğiYıldız Teknik ÜniversitesiÇevre Mühendisliği Ana Bilim Dalı
PROF. DR. MEHMET ÇAKMAKCI
- Köpeklerde dijitoksinle akut zehirlenmelerde kolestiramin ve aktif kömürün koruyucu etkilerinin araştırılması
Başlık çevirisi yok
İ. HALİL SÖZMEN
- Eu2O3, Ho2O3 ve Tb4O7 katkılı Bi2O3 elektrolit malzemenin yapısal ve elektriksel özelliklerinin araştırılması
Investigation of the structural and electrical properties of Eu2O3, Ho2o3 and Tb4O7 doubled Bi2O3 electrolyte material
SİBEL CERİT
Yüksek Lisans
Türkçe
2023
Fizik ve Fizik MühendisliğiErciyes ÜniversitesiFizik Ana Bilim Dalı
PROF. DR. BUKET SAATÇİ
- Design and construction of a secure id-card system using robust image hashing
Gürbüz görüntü işleme ile güvenli kimlik doğrulama sistemi tasarımı ve yapımı
MEHMET ÖZTEMEL
Yüksek Lisans
İngilizce
2009
Elektrik ve Elektronik MühendisliğiBoğaziçi ÜniversitesiElektrik-Elektronik Mühendisliği Ana Bilim Dalı
DOÇ. DR. M. KIVANÇ MIHÇAK