Older news
2019
- 1 October 2019
- Welcome to Jérémy Ledent and Bruno Gavranović, who have joined the MSP group as a postdoc and a PhD student, respectively.
- 1 September 2019
- Radu Mardare is joining the MSP group. Welcome Radu!
- 5 – 9 August 2019
- We are organising the first ever Scottish Programming Languages and Verification Summer School.
- 3 June 2019
- Welcome to Adam Katona and Zachary Sole, who are doing summer internships in the MSP group this year, supervised by Clemens Kupke and Fredrik Nordvall Forsberg respectively.
- 29 May 2019
- Dan Ghica visiting.
- 10 May 2019
- Troels Henriksen visiting.
- 26 March – 1 April 2019
- Johannes Marti visiting.
- 11 March 2019
- Welcome back Guillaume Allais who is starting a postdoc with Conor McBride and Neil Ghani.
2018
- 17 – 18 December 2018
- We are organising SYCO 2, the Second Symposium on Compositional Structures.
- 14 December 2018
- Robin Cockett visiting.
- 30 November 2018
- Congratulations to Kevin Dunne for successfully passing his PhD viva!
- 17 October 2018
- We are organising a meeting of the Scottish Programming Languages Seminar.
- 1 October 2018
- Welcome to Malin Altenmüller who is starting a PhD in the MSP group.
- 27 – 31 August 2018
- Philippa Cowderoy visiting.
- 9 August 2018
- Ron Garcia visiting.
- 16 – 20 July 2018
- Jurriaan Rot visiting.
- 28 May 2018
- Artem Shinkarov visiting.
- 14 – 30 May 2018
- Helle Hvid Hansen visiting.
- 27 – 28 March 2018
- Thorsten Altenkirch visiting.
- 21 March 2018
- Jamie Gabbay visiting.
- 7 February 2018
- Justin Hsu visiting.
- 22 – 26 January 2018
- Jurriaan Rot visiting.
2017
- 6 December 2017
- Chung-Kil Hur visiting.
- 23 – 27 October 2017
- Johannes Marti visiting.
- 11 September 2017
- Andrea Vezzosi visiting.
- 27 July 2017
- Matteo Cavaliere visiting.
- 10 – 11 July 2017
- We are organising a Workshop on Open Games.
- 5 July 2017
- Noam Zeilberger visiting.
- 30 June 2017
- Danel Ahman visiting.
- 26 – 30 June 2017
- Stephan Spahn visiting.
- 10 – 12 April 2017
- We are organising the eighth edition of the workshop Algebra and Coalgebra meet Proof Theory.
- 6 February 2017
- Ohad Kammar visiting.
2016
- 30 November 2016
- We are organising the second meeting Categories, Logic, and Physics, Scotland.
- 21 – 25 November 2016
- Yde Venema and Helle Hvid Hansen visiting.
- 9 November 2016
- We are organising a meeting of the Scottish Programming Languages Seminar.
- 3 October 2016
- Welcome to Alasdair Lambert and Simone Barlocco who are starting PhDs in the MSP group.
- 15 – 16 September 2016
- Jules Hedges visiting.
- 12 September 2016
- Congratulations to Federico Orsanigo for successfully defending his thesis "Bifibrational parametricity: from zero to two dimensions"!
- 12 – 13 September 2016
- Alex Simpson visiting.
- 5 – 9 September 2016
- Stephan Spahn visiting.
- 20 – 26 April 2016
- We are organising the 33rd Agda Implementors’ Meeting at Strathclyde.
- 29 February – 2 March 2016
- Stephan Spahn visiting.
- 26 January 2016
- Aleks Kissinger visiting.
- 25 – 29 January 2016
- John Power visiting.
2015
- 18 November 2015
- Bram Westerbaan visiting.
- 19 – 23 October 2015
- Viktor Winschel visiting.
- 5 – 9 October 2015
- Alessandra Palmigiano visiting.
- 30 September 2015
- Welcome to Ben Price who is starting a PhD under the supervision of Neil Ghani.
- 23 – 25 September 2015
- Pierre Lescanne visiting.
- 14 – 18 September 2015
- Giovanni Cina visiting.
- 25 – 29 August 2015
- Julian Hedges visiting.
- 13 August 2015
- Jeremy Siek visiting.
- 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.
- 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/ - 4 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