COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Kleisli Arrows of Outrageous Fortune

## Kleisli Arrows of Outrageous FortuneAdd to your list(s) Download to your calendar using vCal - Conor McBride, University of Strathclyde
- Friday 11 February 2011, 14:00-15:00
- Room FW11, Computer Laboratory, William Gates Building.
If you have a question about this talk, please contact Bjarki Holm. When we program to interact with a turbulent world, we are to some extent at its mercy. To achieve safety, we must ensure that programs act in accordance with what is known about the state of the world, as determined dynamically. Is there any hope to enforce safety policies for dynamic interaction by static typing? This talk answers with a cautious `yes’. Monads provide structure and a type discipline for effectful programming, mapping value types to computation types. If we index our types by data approximating the `state of the world’, we refine our values to witnesses for some condition of the world. Ordinary monads for indexed types give a discipline for effectful programming contingent on state, modelling the whims of fortune in way that Atkey’s indexed monads for ordinary types do not. Arrows in the corresponding Kleisli category represent computations which a reach a given postcondition from a given precondition: their types are just specifications in a Hoare logic! By way of an elementary introduction to this approach, I present the example of a monad for interacting with a file handle which is either `open’ or `closed’, constructed from a command interface specfied with Hoare-style pre- and postconditions. An attempt to open a file results in a state which is statically unpredictable but dynamically detectable. Well typed programs behave accordingly in either case. Haskell’s dependent type system, as exposed by the Strathclyde Haskell Enhancement preprocessor, provides a suitable basis for this simple experiment. This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Cambridge talks
- Computer Laboratory talks
- Computing and Mathematics
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- Room FW11, Computer Laboratory, William Gates Building
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsPhilosophy and History of Science Department of Geography - main Departmental seminar series Nineteenth-Century Epic## Other talksCoatable photovoltaics (Title t o be confirmed) Small Opuntioideae The Partition of India and Migration Beyond truth-as-correspondence: realism for realistic people Faster C++ Computing knot Floer homology Mathematical applications of little string theory Inferring the Evolutionary History of Cancers: Statistical Methods and Applications Unbiased Estimation of the Eigenvalues of Large Implicit Matrices Diagnostics and patient pathways in pancreatic cancer |