Presentations

It is the custom of the Foundations and Methods Group to have regular presentations by members of the groups on topics they have encountered during their research that are of general interest. Below are the slides of the presentations I have given, in reverse chronological order.

Fixed-Point vs Proof Theoretic Approach to Inference Systems. Notes

We recall the basic definitions and results of elementary fixed point theory: we show that the least fixed point of a monotone function F over a powerset is given by the intersection of all F-closed sets, and dually that the greatest fixed point of F is given by the union of all F-consistent sets. We recall the definitions of continuity and cocontinuity, give an alternative construction of least and greatest fixed points for continuous and cocontinuous functions, and give examples of non-continuous and non-cocontinuous functions. We recall the definition of an inference system Φ, show that the associated function F_Φ is always monotone and hence has a least fixed point μF_Φ (the inductive interpretation of Φ) and greatest fixed point νF_Φ (the coinductive interpretation of Φ). We give conditions over Φ that guarantee that F_Φ is continous or cocontinuous, and give examples of inference systems that do not meet these conditions. We show that the inductive and coinductive interpretation of Φ give rise to the proof principles of rule induction and Park's principle. Finally, we show that the set ΔΦ of the conclusions of finite proofs over Φ corresponds to the inductive interpretation of Φ, and dually that the set ∇Φ of the conclusions of finite and infinite proofs over Φ corresponds to its coinductive interpretation; i.e. that μF_Φ = ΔΦ     and     νF_Φ = ∇Φ The results in this report are not new, but we hope the reader finds the exposition and examples useful.

Ordinals. Slides

(Countable) ordinal numbers are an extension of the natural numbers to cover infinite numbers. Yet, "ordinal induction" or "transfinite induction" is well-founded (and transfinite recursion terminates). Moreover, ordinals can be used in termination arguments. We try to give an intuitive explanation of the countable ordinals and show how a process can meaningfully be said to 'terminate in omega' (or more..) steps. We also briefly discuss cardinals and uncountable ordinals.

Introduction to Uniqueness Typing. Slides

High-level introduction to the functional approach to tackling side effects using substructural logic. Discusses terminology (e.g., what is referential transparency?), introduces uniqueness typing and monads and compares them, gives a general introduction to the Curry-Howard isomorphism and substructural logic, and as ``bonus track'' briefly discusses circular programming. Given as part of the Foundations@Lero seminar series.

Partiality for Dummies.

An accessible introduction to the partiality monad. Unfortunately, the slides give a definition of a fixpoint in the partiality monad which I shamelessly stole from Edwin Brady's SK Combinator Calculus Interpreter. As it turns out, this definition is good enough for the SK interpreter but it is unsuitable as a general definition of a the fixpoint combinator since it will cause unnecessary non-termination in some function definitions. For the general definition, see Partiality is an Effect (what we are missing is something like their omegarace) or Capretta's paper General Recursion via Coinductive Types (where omegarace is called parallel_search). To avoid further spreading of this definition, the slides are no longer available. If anyone wants to have a copy, please contact me. Apologies.

Monomorphic Type Systems for the Pi-calculus. Slides , Bibliography

Discusses a number of type systems suggested by Kobayashi for the pi-calculus.

Separation logic. Slides , Bibliography

Discusses imperative separation logic, its extension to concurrent imperative programs, the logic behind it (bunched implications) and briefly mention applications to process calculi.

Abstract Nonsense for Functional Programmers. Slides

Discusses basic category theory (categories, functors, Hom functors, algebras, monads, natural transformations, and the Yoneda lemma) from a functional programmer's perspective. (The talk also briefly discussed the partiality monad, but I removed those two slides as they contained the erroneous fixpoint definition mentioned above for Partiality for Dummies.)

Recursion Patterns. Slides

Introduces recursion patterns in functional programming (catamorphism, anamorphism, hylomorphism, paramorphism) and compares them to induction patterns in theorem proving. Looks in some detail at various induction patterns and shows that they are folds (or explicit recursion).

Linear Logic and Uniqueness Typing. Slides

Introducing linear and affine logic, shows how linear logic can be used as a type system, and briefly compares linear logic to uniqueness typing.

(Temporal) Logic Tutorial. Notes

Recaps basic definitions from propositional and first order predicate logic, then introduces temporal logic and shows one application of temporal logic in compiler design.

Dijkstra's Weakest Precondition. Slides

Explains the weakest precondition theory based on Dijkstra's Discipline of Programming.

Generic Programming in Clean. Slides

Explains some of the basic (category) theory behind generic programming and how it is applied in Clean.

Graph Reduction: The Implementation of Functional Languages. Slides .

Talk based mainly on The Implementation of Functional Programming Languages by Simon Peyton Jones.