Capsules and non-well-founded computation
Jean-Baptiste Jeannin · eCommons (Cornell University) · 2013
Several recent programming languages, for example Python, C# and Javascript, are not strictly imperative or functional, but provide features from both paradigms.In this dissertation, we introduce capsules, an algebraic representation of the state of a computation in such higher-order functional and imperative languages.A capsule is essentially a finite coalgebraic representation of a regular closed λ-coterm.One can give an operational semantics based on capsules for a higher-order programming language with functional and imperative features, including mutable bindings.Static (lexical) scoping is captured purely algebraically without stacks, heaps, or closures.Definitions and applications of functions, including recursive functions, are typable with simple types, yet the language is Turing complete.Recursive functions are represented directly as capsules without the need for fixpoint combinators.In this disseration we precisely compare a capsule-based semantics to a closure-based semantics.We also study a formulation of separation logic using capsules, prove soundness of the frame rule in this context and investigate alternative formulations with weaker side conditions.This thesis would never have been possible without my advisor, Dexter.I learnt so much by your side!You are an amazing teacher, because you really care about teaching and never get tired of explaining the same thing again and again.What always impresses me the most is your constant ability to give me a mini-lecture about any topic about which I had asked a question, without preparing or looking up anything.You also have an extremely balanced life, between family, research, sports and music, and I hope to achieve such balance in my life too.Thank you for being such an example!I would also like to thank the other members of my committee, Ashutosh, Hadas and Nate, for always being available when I wanted to chat or ask more general questions about my Ph.D. or my future.Alexandra, you have become much more than a co-author but a real friend.You arrived as a postdoc with Dexter at a moment when I needed some encouragements and new research directions, and you sure provided that!Thank you so much for always being there to listen, be it in Ithaca, Amsterdam or Nijmegen, and for hosting me in the Netherlands twice.I hope to keep you as a