Mathematically Structured Programming Group

Computer and Information Sciences

University of Strathclyde

Older News

2015

25 – 27 May 2015
Paul Levy visiting.
20 March 2015
Chris Heunen visiting.
4 March 2015
We are organising A HoTT-Date with Thorsten Altenkirch — an afternoon of talks.
2 – 6 March 2015
Thorsten Altenkirch visiting.
20 – 23 January 2015
James Chapman visiting.

2014

9 – 10 December 2014
Aleks Kissinger visiting.
26 September – 3 October 2014
Helle Hvid Hansen visiting.
30 September 2014
Welcome to Kevin Dunne who is starting a PhD under the supervision of Ross Duncan.
23 – 24 June 2014
Upcoming event: Workshop on Fibrations in Computer Science organised at Strathclyde.
4 – 6 June 2014
The SICSA theme event Practical Types is organised by Neil and others, and attended by many of the MSP group.
28 – 29 May 2014
Ohad Kammar visiting.
22 May 2014
Homotopy Type Theory reading group session on Higher Inductive Types will meet at Strathclyde.
15 April 2014

James Brotherston visiting and giving a talk in the Departmental seminar at 3pm in room LT14.15 about Parametric completeness for separation theories (via hybrid logic).

Abstract: In this talk, we consider the logical gap between the following two concepts:

(1) provability in a propositional axiomatisation of separation logic, which is usually given by the bunched logic BBI; and

(2) validity in an intended class of models of separation logic, as commonly considered in its program verification applications. Such intended classes are usually specified by a collection of algebraic axioms describing specific model properties, which we call a separation theory.

Here, we show first that several typical properties of separation theories are in fact not definable in BBI. Then, we show that these properties become definable in a natural hybrid extension of BBI, obtained by adding a theory of naming to BBI in the same way that hybrid logic extends normal modal logic. Finally, we show how to build an axiomatic proof system for our hybrid logic in such a way that adding any axiom of a certain form yields a sound and complete proof system with respect to the models satisfying those axioms. In particular, this yields sound and complete proof systems for any separation theory from our considered class (which, to the best of our knowledge, includes all those appearing in the literature).

This is joint work with Jules Villard, now at Imperial.

9 April 2014

David Aspinall visiting and giving a talk in the Departmental seminar about Managing Proofs Hierarchically.

Abstract: For the past several years, we have been studying the notion of hiproofs as a foundation for proof objects with hierarchical structure. The idea is that a theorem proving tool produces an internal representation that can be inspected, navigated and manipulated as a hiproof. I'll give a review of the syntactic and denotational formulations of hiproof, and the proof and manipulation languages we have designed on top. I'll describe upcoming work which will build on this, including the new ProofPeer project on collaborative theorem proving.

7 April 2014
Jamie Gabbay visiting.
31 March – 4 April 2014
Thorsten Altenkirch visiting.

2013

16 August 2013
Dr Robin Adams will be joining the MSP group as an Academic Visitor for the academic year 2013-2014. Robin will (probably) be working on logic enriched type theory, but I'm sure we will have plenty of other points of intersection.
12 August 2013
Neil Ghani has been awarded a SICSA Distinguished Fellowship to host Andy Gill in October/November 2013 for two weeks. Andy will be giving a number of lectures around Scotland on Domain Specific Languages so let us know if you are interested in attending them.
4 August 2013
The MSP group, as part of a consortium of research groups, has been awarded an EU-travel grant to make multiple visits to CMU (Steve Awodey and Bob Harper) in the US and ANU (Dirk Pattinson) in Australia over the period 2014-2017. Time to pack our bags!
29 July 2013
We are currently looking for a new Lecturer or Senior Lecturer within the MSP group. See the above link for how to apply (deadline is 8 September 2013). Ideally we are looking for someone who
  • Fits - at least a little - into what we do now which is roughly category theory in CS (Neil), functional programming and type theory (Conor) and databases and coalgebra (Clemens)
  • Offers us something new and exciting that we ought to have some strength in but don't.
  • Knows how to - or has the capacity to learn how to - get grants. We have big plans for the group but can only bring them to fruition if we show we can fund fellowships and RAs.
23 July 2013
Alwin Blok will be joining the MSP group to study for a PhD under Clemens expert supervision.
23 May 2013
Dr Johann and Prof Ghani have been awarded a 4-year EPSRC grant "Logical Relations for Program Verification". We are pleased to say that Fredrik Nordvall Forsberg has agreed to join us as an RA on this grant and will join the MSP group on 1 December 2013. Welcome Fred!
22 May 2013
Patricia Johann is organising this year's Parametricity Workshop at Strathclyde.
1 January 2013
Clemens Kupke has taken up a lectureship position within the group.

2012

3 October 2012
Welcome to Federico Orsanigo and Tim Revell, starting their PhD studies in the MSP group. Federico is being supervised by Patricia Johann and Tim is being supervised by Neil Ghani.
15 June 2012
Lectureship in the Mathematically Structured Programming Group

Applications are invited for lectureship within the MSP group at the University of Strathclyde The applicant's motivation must centre on a desire to discover beautiful mathematics of lasting value. The applicant should also have an innate sense of the wonder of learning allied with the capacity for self-motivation and a track record of academic achievement.

The Mathematically Structured Programming Group's vision is to use mathematics to understand the nature of computation, and to then turn that understanding into practical advances within programming languages research. This reflects the symbiotic relationship between mathematics, programming, and the design of programming languages --- we believe that any attempt to sever this connection will diminish each component. In order to achieve these research goals, we mainly use ideas from category theory, type theory, and functional programming. The group consists of a number of internationally leading researchers including Professor Neil Ghani, Dr Patricia Johann, Dr Conor McBride, Dr Peter Hancock, Dr Robert Atkey, and our PhD students.

While the lectureship is formally in the area of Program Verification, this is to be interpreted broadly. Very broadly. Anyone interested should in the first instance contact Professor Neil Ghani, whose email address is "neil.ghani at strath.ac.uk" to register interest. Details of the position can be found at http://www.mis.strath.ac.uk/Personnel/open/712012.pdf.

The closing date for applications is Thursday July 26.

15 June 2012
Upcoming event: International Workshop on 75 Years of the λ-Calculus
1 June 2012
Congratulations to Clement Fumex on passing his viva! Clement's thesis is entitled "Induction and Coinduction schemes in Category Theory". His examiners were Bart Jacobs (external) and Conor McBride (internal). Clement's thesis was supervised by Patty Johann.
25 May 2012
Upcoming event: 6th Scottish Category Theory Seminar.
2 May 2012
Event: Parametricity Workshop
7 March 2012
PhD Position: Higher Dimensional Categories and Types

Applications are invited for PhD study under the supervision of Prof Neil Ghani on any topic relating to higher dimensional category theory and/or higher dimensional type theory. The position is fully funded for EU students (apologies to non EU-citizens for this ridiculous piece of non-meritocracy) and will last for 3 years.The applicant's motivation must centre on a desire for beautiful mathematics of lasting value. The applicant should also have an innate sense of the wonder of learning allied to the capacity to work hard and achieve their goals.

The Mathematically Structured Programming Group's vision is to use mathematics to understand the nature of computation, and to then turn that understanding into the next generation of programming languages. This reflects the symbiotic relationship between mathematics, programming, and the design of programming languages — any attempt to sever this connection will diminish each component. In order to achieve these research goals we mainly use ideas from category theory, type theory and functional programming. Besides Professor Neil Ghani, the group consists of a number of internationally leading researchers including Dr Patricia Johann, Dr Conor McBride, Dr Peter Hancock, Dr Robert Atkey as well as a number of PhD students.

Anyone interested should in the first instance contact Professor Neil Ghani whose email address is "ng at cis.strath.ac.uk" and outline their academic background. Applications will be considered on a first come, first served basis.

10 February 2012
Scottish Theorem Provers Meeting

2011

19 December 2011
Peter Hancock at 60

We had a day of talks to celebrate Peter Hancock's 60th Birthday.

More information.

25 November 2011
5th Scottish Category Theory Seminar
16 August 2011
6 Month Postdoc Position

Mathematically Structured Programming Group
University of Strathclyde
Scotland

We have the potential to apply for funds for a 6 month post doctoral position. The idea is that the successful candidate would spend those 6 months writing a full scale grant to fund themselves for the next 3 years.

The postdoctoral position would be within the Mathematically Structured Programing group at the University of Strathclyde whose research focusses on category theory, type theory and functional programming. Current staff include Neil Ghani, Patricia Johann, Conor McBride, Peter Hancock, Robert Atkey and 6 PhD students.

The candidate we are looking for should be highly self motivated and appreciate that without beauty, we are lost.

Unfortunately, the deadline is extremely short and so any interested candidates should contact me immediately. I can then tell you more about what we would need to do.

For more information, please contact:

Professor Neil Ghani
ng@cis.strath.ac.uk
http://personal.cis.strath.ac.uk/~ng/
http://msp.cis.strath.ac.uk/

4th August 2011
Prakash Panangaden talk. 2pm.

Title: The Duality of State and Observation

Abstract: In this talk we consider the problem of representing and reasoning about systems, especially probabilistic systems, with hidden state. We consider transition systems where the state is not completely visible to an outside observer. Instead, there are observables that partly identify the state. We show that one can interchange the notions of state and observation and obtain what we call a dual system. The double dual gives a minimal representation of the behaviour of the original system. We extend this to nondeterministic systems and to probabilistic transition systems and finally to partially observable Markov decision processes (POMDPs). In the case of finite automata restricted to one observable, we obtain Brzozowski's algorithm for minimizing finite-state language acceptors. This is joint work with colleagues from McGill: Doina Precup and Joelle Pineau and my former student Chris Hunt.

1 – 2 June 2011
Bart Jacobs visited.
17 May 2011
Phil Scott talk.

Title: Traced categories: algebraic structure of feedback and partial feedback in networks

Abstract: In the late '80s/early '90s an algebraic structure dealing with cyclic operations emerged from various fields, including flowchart schemes, dataflow networks with feedback, action calculi, proof theory, as well as algebraic topology and knot theory. This structure is now known as a "traced monoidal category" , after the influential paper of Joyal, Street and Verity, who studied such categories in pure mathematics, but with an eye to applications in many fields. The concept also occurs as a basic structure in network algebra. Since then, these categories have been studied, with variations, in many areas of mathematics, logic and theoretical computer science, Recently, there has been a trend to consider partial traces and trace ideals; indeed it appears that such algebraic structures may be relevant to several areas, including biology and physics, or indeed to any field where cyclic networks are used. We give an introduction to the subject, along with some recent advances.

13 May 2011
4th Scottish Category Theory Seminar
21 – 25 April 2011
Janis Voigtländer visited.
17 February 2011
Nicola Gambino talk. 12pm. Location 14.15.

Title: Voevodsky's Univalence Axiom

Abstract: Vladimir Voevodsky has recently introduced a semantics for constructive type theory in which types are interpreted as simplicial sets. This semantics validates not only the usual rules for identity types but also an additional rule, called the Univalence Axiom. The aim of the talk is to explain the statement of the Univalence Axiom and outline Voevodsky's proof that it implies a form of function extensionality.

2010

3 December 2010
Algebraic Set Theory Course: Benno van den Berg
2 December 2010
3rd Scottish Category Theory Seminar
22 – 26 November 2010
Wouter Swierstra visiting.
24 November 2010
Scottish Programming Languages Seminar