[logic-ml] Talks by Georg Struth (29 May) & by Bart Jacobs (2 Jun) at U Tokyo

[Ichiro Hasuo]

Dear colleagues,

Let me advertise talks given by our guests: Georg Struth on algebraic
techniques in program analysis; and Bart Jacobs on categorical quantum
logic. No registration is necessary; see you there!

Best regards,
Ichiro Hasuo
Group website: http://www-mmm.is.s.u-tokyo.ac.jp/


________________________________

Thu 29 May 2014, 16:30-18:00

Georg Struth (U. Sheffield), Build Your Own Program Analysis Tool

理学部7号館2階 214教室   Room 214, School of Science Bldg. No. 7

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access: http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)


We present a principled way of designing program analysis tools within
interactive proof assistants such as Coq or Isabelle; inparticular
tools for the construction and verification of sequential and
concurrent programs. We use algebras of programs to capture the
control flow of programs and to derive Hoare-style inference rules,
verification conditions, or transformation and refinement laws. We
model their data flow by linking these algebras with denotational
models of programs, including relations, predicate transformers, or
sets of traces and by enriching these with notions of store and state,
with data types, assignment and process interference.


This separation of concern makes the approach open, modular and highly
automatic. Its implementation in Isabelle/HOL is particularly simple.
It yields lightweight tools which are themselves correct by
construction and can be combined with various programming languages
and integrated into different formal methods.


We illustrate the approach through three examples: a verification tool
for while programs based on Kleene algebra with tests, its extension
to a Morgan-style program refinement tool, and a prototype for
verifying and constructing shared variable concurrent programs based
on a new variant of concurrent Kleene algebra. Time permitting, we

will outline how more powerful program analysis tools can be obtained
from more expressive algebras.


________________________________

Mon 2 Jun 2014, 15:30-17:00

Bart Jacobs (Radboud U. Njimegen), Axiomatising categorical quantum logic

化学東館 236教室（理学部7号館の隣．ご存知ない方は先に理学部7号館415へお越しください）
Room 236, Chemistry Building East (“Kagaku-Higashikan”). If not
familiar come first to Rm 415, School of Science Bldg. No. 7

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access: http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)


This talk describes several assumptions on a category that together
yield a proposal for a categorical structure for quantum logic. The
assumptions and consequences describe the differences and similarities
between classical, probabilistic, and quantum logic. The leading
examples are the category Sets, the Kleisli category of the
distribution monad, and the opposite of the category of C*-algebras
and (completely) positive unital maps.