An Exercise in Formalisation: Blockchain Transactions

11/8/2018
application/pdf iconslides.pdf

By Steve Reeves, University of Waikato (New Zeeland)

Abstract:
 Notions of guardedness serve to delineate admissible recursive definitions in various settings in a compositional manner. To formalize this, a unified axiomatic notion of guardedness in symmetric monoidal categories emerged recently, covering various examples from program semantics, process algebra, hybrid computations and beyond -- the list is being completed on an on-going basis. Here, I present a metalanguage for guarded iteration based on combining axiomatic guardedness with the popular fine-grain call-by-value paradigm, intended as a unifying programming language for guarded and unguarded iteration in the presence of computational effects. I give a generic (categorical) semantics for this language over a suitable class of .

About the Speaker:
I started my career a long time ago in automated theorem-proving (using semantic tableaux, in the days when resolution was considered to be the only respectable technique), and then moved into formal methods (at the University of Essex and then QMC, University of London) around non-standard logics, especially intuitionistic/constructive ones, before a move to the University of Waikato in New Zealand. In the past I did a lot of work with Martin Henson on the semantics of and a logic for Z, but rather more recently I have been working on building and investigating models for small medical devices, and even more recently I have started to look at formalisation of blockchain systems, as well as their use as a basis for storing cultural artefacts and considering the governance and trust issues that such a use entails.

LOCATION AND TIME

Address:  University of Minho, Gualtar Campus, Braga, Portugal

Building: Departamento de Informatica, Building 07

Networking Session: 1:45PM-2PM, Auditorium A2, 1st floor

Talk Session: 2PM-3PM, Auditorium A2, 1st floor

PHOTOS