Monaadid programmeerimises ja verifitseerimisel (kevad 2008)

Registreerumine: Meiliga Tarmo Uustalule aadressil firstname(at)cs.ioc.ee. Tähtaeg: 21.5.2008 kl 17.00.

Kood: ITT9204

Punkte: 1.5 AP

Tunde: 6 tundi loenguid

Tunniplaan: loengud E 26.5 kl 14-15.30, T 27.5 kl 10-11.30 ja 14-15.30 Küberneetika Maja (Akadeemia tee 21) (NB! plaan, võib muutuda)

Kontrollivorm: eksam

Eksam: Eksamihinde saamiseks tuleb teostada miniprojekt. Tähtaeg R 6.6.2008!

Õppejõud: dr. Ralph Matthes, IRIT, Université Paul Sabatier (Toulouse 3)

Kontakt: Tarmo Uustalu, firstname(at)cs.ioc.ee, 620 4250

Kursus toimub RAKi Meetme 1.1 IKT doktorikooli projekti raames.

Monads for programming and verification

Dr. Ralph Matthes
Institut de Recherche en Informatique de Toulouse (IRIT)
Université Paul Sabatier (Toulouse 3)

Abstract

The tutorial has three axes, based on the following three papers:

  1. S. Peyton Jones. Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. In T. Hoare, M. Broy, R. Steinbruggen, eds., Engineering theories of software construction, pp. 47-96, IOS Press, 2001. Updated afterwards. author's version

    This is a Marktoberdorf tutorial on the practical usage of monads for programming in Haskell with effects. Nevertheless, an operational semantics is included that helps with a more formal understanding.

  2. S. Peyton Jones, D. Vytiniotis, S. Weirich, M. Shields. Practical type inference for arbitrary-rank types. J. of Funct. Program., v. 17, n. 1, pp. 1-82, 2007. doi: 10.1017/s0956796806006034

    This paper that admittedly is "strongly tutorial in style" presents an excellent case for monadic programming: Damas-Milner type inference plus extensions by type annotations, bidirectionality and higher ranks. The monad holds all the binding for the meta type variables and manages exceptions and the environment (but the latter not by side-effect).

  3. A. Filinski. On the relations between monadic semantics. Theor. Comput. Sci., v. 375, pp. 41-75, 2007. doi:10.1016/j.tcs.2006.12.027

    This article in the Reynolds Festschrift updates Reynolds' work from the 70ies on proving agreement of different semantics for untyped languages. The framework is now a multi-monadic metalanguage with sub-effecting, and direct and continuation semantics for a toy language with call-by-value and call-by-name lambda-abstraction are represented with monads and shown to agree for closed expressions.

(All fulltexts available from within TUT computer network.)

Course material

Tarmo Uustalu
Viimane uuendus 13.5.2008