| ชื่อเรื่อง | : | Logic and handling of algebraic effects |
| นักวิจัย | : | Pretnar, Matija |
| คำค้น | : | computational effects , algebraic theories , program logics , exception handlers |
| หน่วยงาน | : | Edinburgh Research Archive, United Kingdom |
| ผู้ร่วมงาน | : | Plotkin, Gordon , Power, John , Engineering and Physical Sciences Research Council (EPSRC) |
| ปีพิมพ์ | : | 2553 |
| อ้างอิง | : | http://hdl.handle.net/1842/4611 |
| ที่มา | : | - |
| ความเชี่ยวชาญ | : | - |
| ความสัมพันธ์ | : | Gordon David Plotkin and Matija Pretnar. A logic for algebraic effects. In 23rd Symposium on Logic in Computer Science, pages 118-129, 2008. , Gordon David Plotkin and Matija Pretnar. Handlers of algebraic effects. In ESOP 2009, volume 5502 of Lecture Notes in Computer Science, pages 80–94, 2009. |
| ขอบเขตของเนื้อหา | : | - |
| บทคัดย่อ/คำอธิบาย | : | In the thesis, we explore reasoning about and handling of algebraic effects. Those are computational effects, which admit a representation by an equational theory. Their examples include exceptions, nondeterminism, interactive input and output, state, and their combinations. In the first part of the thesis, we propose a logic for algebraic effects. We begin by introducing the a-calculus, which is a minimal equational logic with the purpose of exposing distinct features of algebraic effects. Next, we give a powerful logic, which builds on results of the a-calculus. The types and terms of the logic are the ones of Levy’s call-by-push-value framework, while the reasoning rules are the standard ones of a classical multi-sorted first-order logic with predicates, extended with predicate fixed points and two principles that describe the universality of free models of the theory representing the effects at hand. Afterwards, we show the use of the logic in reasoning about properties of effectful programs, and in the translation of Moggi’s computational ¸-calculus, Hennessy-Milner logic, and Moggi’s refinement of Pitts’s evaluation logic. In the second part of the thesis, we introduce handlers of algebraic effects. Those not only provide an algebraic treatment of exception handlers, but generalise them to arbitrary algebraic effects. Each such handler corresponds to a model of the theory representing the effects, while the handling construct is interpreted by the homomorphism induced by the universal property of the free model. We use handlers to describe many previously unrelated concepts from both theory and practice, for example CSS renaming and hiding, stream redirection, timeout, and rollback. |
| บรรณานุกรม | : |
Pretnar, Matija . (2553). Logic and handling of algebraic effects.
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom . Pretnar, Matija . 2553. "Logic and handling of algebraic effects".
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom . Pretnar, Matija . "Logic and handling of algebraic effects."
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom , 2553. Print. Pretnar, Matija . Logic and handling of algebraic effects. กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom ; 2553.
|
