Show simple item record

dc.contributor.authorCenciarelli , Pietro
dc.date.accessioned2004-03-03T12:22:04Z
dc.date.available2004-03-03T12:22:04Z
dc.date.issued1996-07
dc.identifier.urihttp://hdl.handle.net/1842/396
dc.description.abstractThis thesis studies various manifestations of monads in the mathematics of computation and presents three applications of calculi based on monads. The view that monads provide abstract mathematical interpretations of computational phenomena led E. Moggi to use the internal language of a category with a strong monad, which he called the computational lambda calculus, for describing denotational semantics of programming languages. Moggi argued that models of complicated forms of computation could be described modularly by using semantic constructors for manipulating monads. For the first application, we describe a theory of exceptions in the computational lambda calculus and give a computationally adequate interpretation of a fragment of ML, including the exception handling mechanism, in models of this theory. To our knowledge no other model of ML exceptions is available in the literature to date. We also show that normalization fails when exceptions are added to the simply typed lambda calculus. Building on top of the computational lambda calculus, A.M. Pitts proposed a predicate calculus to reason about the evaluation properties of programs: the Evaluation Logic. Following the tenets of synthetic domain theory, we interpret this logic in an ambient category with set-like structure and a fully reflective subcategory of domains with a monad for interpreting computation. We establish abstract conditions under which the monad extends to the ambient category to ensure good interaction with the logical structure. We also show that a monad and first order logical structure yield suitable evaluation relations, which can be used to give a standard interpretation of Evaluation Logic when higher order structure is not available. For the second application, we focus on side effects and investigate the use of Evaluation Logic in partial correctness reasoning. We show that, under fairly common circumstances, monads for side effects admit an extension to the ambient category which is more natural than that described for arbitrary monads and we validate special axioms for members of this class. The resulting theory of computation with side effects is then put to work on a textbook example of partial correctness specification. For our third application, we consider Moggi's modular approach to denotational semantics. We develop the theory of this approach by determining which equations are preserved by a fairly general class of semantic constructors and which ones are reflected (conservativity). Moreover, we establish a correspondence between categories of computational models and categories of theories of the metalanguage, along the lines of Gabriel-Ulmer duality, in a type-theoretic framework. Using the Extended Calculus of Constructions, we develop a semantics for parallel composition by combining elementary notions of computation defined independently and we use LEGO to prove properties of such semantics formally.en
dc.format.extent811120 bytes
dc.format.extent2156754 bytes
dc.format.extent1522217 bytes
dc.format.mimetypeapplication/x-dvi
dc.format.mimetypeapplication/pdf
dc.format.mimetypeapplication/postscript
dc.language.isoen
dc.publisherUniversity of Edinburgh. College of Science and Engineering. School of Informatics.en
dc.titleComputational applications of calculi based on monadsen
dc.typeThesis or Dissertation
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record