We present a logic for algebraic effects generalising Scott's LCF; it is based on the algebraic representation of computational effects by operations and equations. The logic is a classical first- order multi-sorted logic; its terms include Moggi’s computational λ-calculus, and it has a principle of induction over computations, a free algebra principle, and predicate fixed points. This logic embraces Hennessy-Milner logic, and evaluation logic via definable modalities; however Hoare logic presents difficulties.
This is joint work with Matija Pretnar
It is well known that all initial algebras support well-behaved recursion operators. Sadly, our understanding of induction is not so well understood. In this talk I will show that all initial algebras support induction principles for reasoning about properties which are fibred over a base category of types.
This is joint work with Patricia Johann and Clement Fumex
It turns out that by using ideas from modal logic you can build models of the lambda-calculus. Lambda corresponds to a logical quantifier and reduction corresponds to logical entailment. The models are sound and complete. See also the LPAR'10 paper.
This is joint work with Michael Gabbay.
One popular notion of a (Scott-Ershov) domain is defined as a bounded complete algebraic cpo. Such an abstract definition is not always so helpful for beginners. The speaker found recently that there is an easy-to-construct domain of countable semilattices giving isomorphic copies of all countably based domains. This approach seems to have advantages over both the so-called "information systems" and more abstract lattice/ topological formulations, and it makes definitions of solutions to domain equations very elementary to justify. The "domain of domains" also has a natural computable structure.