_news.yaml

- date: 4 November 2024
  description:
    We are looking for <a href="/phd2025-JARSS.html">funded UK PhD candidates</a> for 2025.

- date: 1 October 2024
  description:
    Welcome to Samuel Fish, who is starting a PhD in the MSP group.

- date: 2 September 2024
  description:
    Welcome to Clovis Eberhart, who is joining the MSP group as a research fellow.

- date: 13 August 2024
  description:
    <a href="https://sites.google.com/uniroma1.it/gorla">Daniele Gorla</a> visiting.

- start: 29 July 2024
  end: 2 August 2024
  description:
    We are hosting the <a href="https://spli.scot/splv/2024-strathclyde/">Scottish Programming Languages and Verification Summer School 2024</a> at Strathclyde.

- date: 17 April 2024
  description:
    <a href="https://www.kcl.ac.uk/people/dov-gabbay">Dov Gabbay</a> visiting.

- start: 4 March 2024
  end: 8 March 2024
  description:
    Paolo Torrens visiting.

- date: 14 February 2024
  description:
    We have a <a href="phd2024.html">PhD position available</a> with a start date of 1 October 2024.

- date: 13 February 2024
  description:
    <a href="https://www.cs.ox.ac.uk/people/nobuko.yoshida/">Nobuko Yoshida</a> is visiting.

- date: 29 January 2024
  description:
    Congratulations to Joe Collins for successfully passing his
    PhD viva with minor corrections!

- date: 12 January 2024
  description:
    Congratulations to James Wood for successfully passing his
    PhD viva with minor corrections!

- date: 04 December 2023
  description:
    We are organising the second Categories Network Project (CATNIP) meeting.

- start: 22 November 2023
  end: 23 November 2023
  description:
    <a href="https://danel.ahman.ee/">Danel Ahman</a> is visiting.

- date: 22 November 2023
  description:
    We are organising the <a href="https://scottish-pl-institute.github.io/spls/meetings/2023/november/">Scottish Programming Languages Seminar</a>.

- date: 22 September 2023
  description:
    Congratulations to Bruno Gavranović for successfully passing his
    PhD viva with minor corrections!

- date: 5 May 2023
  description:
    Welcome to Iwan Qu&eacute;merais, who is doing an internship with
    Clemens Kupke over the summer.

- date: 5 May 2023
  description:
    <a href="http://johannesmarti.com/">Johannes Marti</a> is visiting.

- date: 4 May 2023
  description:
    Welcome to <ahref="https://personal.cis.strath.ac.uk/ethel.morgan/">Ethel
    Morgan</a>, who joined the MSP group as a Research Software
    Engineer.

- date: 14 April 2023
  description:
    <a href="http://www.cs.nott.ac.uk/~txa/">Thorsten Altenkirch</a> visiting.

- date: 1 April 2023
  description:
    Welcome to <a href="https://gallais.github.io/">Guillaume
    Allais</a>, who joined the MSP group as a Chancellor's Fellow.

- date: 29 March 2023
  description:
    <a href="https://www.cs.mcgill.ca/~prakash/">Prakash Panangaden</a> visiting.

- start: 6 March 2023
  end: 14 March 2023
  description:
    <a href="https://headcube.vootrunner.com/">Nathaniel Virgo</a> visiting.

- date: 8 November 2022
  description:
    Congratulations to Guillaume Allais for successfully passing his
    PhD viva with minor corrections!

- start: 1 September 2022
  end: 31 December 2022
  description:
    <a href="https://www.cas.mcmaster.ca/~carette/">Jacques Carette</a> visiting.

- start: 18 July 2022
  end: 22 July 2022
  description:
    We are organising the 5th international conference on
    <a href="https://msp.cis.strath.ac.uk/act2022/">Applied Category
    Theory</a>.

- date: 10 January 2022
  description:
    Welcome to <a href="https://personal.cis.strath.ac.uk/william.waites/">William
    Waites</a>, who joined the MSP group as a Chancellor's Fellow.

- date: 1 October 2021
  description:
    Welcome to Dylan Braithwaite and Sean Watters, who are starting
    PhDs in the MSP group.

- date: 2 September 2021
  description:
    Congratulations to Radu who got the best paper award at <a
    href="https://www.coalg.org/calco-mfps2021/calco/">CALCO 2021</a>,
    for his paper <em>Tensor of Quantitative Equational Theories</em>
    with G. Bacci, P. Panangaden and G. Plotkin.

- date: 1 August 2021
  description:
    <a href="https://sites.google.com/view/jadeedenstarmaster/home/">Jade
    Master</a> has joined the MSP group. Welcome!

- date: 21 July 2021
  description:
    Welcome to Riu Rodríguez Sakamoto, who is starting a PhD in the MSP group.

- date: 1 July 2021
  description:
    Welcome to Ezra Schoen, who is starting a PhD in the MSP group.

- date: 1 October 2020
  description:
    Welcome to André Videla, <a href="https://erischel.com/">Eigil
    Rischel</a> and <a href="https://matteocapucci.wordpress.com/">Matteo
    Capucci</a>, who are starting PhDs in the MSP group.

- date: 25 September 2020
  description:
    Neil is giving weekly tutorial sessions on Open Games for MSP
    newcomers. Video recordings are available <a
    href="./opengames.html">here</a>.

- date: 1 September 2020
  description:
    <a href="https://www.cl.cam.ac.uk/~gw104/">Glynn Winskel</a> and
    <a href="https://julesh.com/">Jules Hedges</a> have joined the MSP
    group. Welcome!

- date: 2 March 2020
  description:
     Welcome to Craig Roy who has joined MSP as a KTP Associate at <a
     href="https://cambridgequantum.com/">Cambridge Quantum Computing</a>.

- date: 6 January 2020
  description:
    Welcome to Georgi Nakov who is starting a PhD under the
    supervision of Fredrik Nordvall Forsberg.

- date: 1 October 2019
  description:
    Welcome to Jérémy Ledent and <a
    href="https://www.brunogavranovic.com/">Bruno Gavranović</a>, who
    have joined the MSP group as a postdoc and a PhD student,
    respectively.

- date: 1 September 2019
  description:
    <a href="https://personal.cis.strath.ac.uk/r.mardare/">Radu
    Mardare</a> is joining the MSP group. Welcome Radu!

- start: 5 August 2019
  end: 9 August 2019
  description:
    We are organising the first ever <a href="http://www.macs.hw.ac.uk/splv/splv19/">
    Scottish Programming Languages and Verification Summer School</a>.

- date: 3 June 2019
  description:
    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.

- date: 29 May 2019
  description:
    <a href="https://www.cs.bham.ac.uk/~drg/">Dan Ghica</a> visiting.


- date: 10 May 2019
  description:
    <a href="http://sigkill.dk/">Troels Henriksen</a> visiting.

- start: 26 March 2019
  end: 1 April 2019
  description:
    <a href="http://johannesmarti.com/">Johannes Marti</a> visiting.

- date: 11 March 2019
  description:
    Welcome back <a href="http://gallais.github.io/">Guillaume
    Allais</a> who is starting a postdoc with Conor McBride and Neil
    Ghani.

- start: 17 December 2018
  end: 18 December 2018
  description:
    We are organising <a href="http://events.cs.bham.ac.uk/syco/2/">SYCO 2</a>, the Second Symposium on Compositional Structures.

- date: 14 December 2018
  description:
    <a href="https://pages.cpsc.ucalgary.ca/~robin/">Robin Cockett</a> visiting.


- date: 30 November 2018
  description:
    Congratulations to Kevin Dunne for successfully passing his PhD viva!


- date: 17 October 2018
  description:
    We are organising a meeting of the <a href='https://msp-strath.github.io/spls-18/'>Scottish Programming Languages Seminar</a>.


- date: 1 October 2018
  description:
    Welcome to Malin Altenm&uuml;ller who is starting a PhD in the MSP
    group.


- start: 27 August 2018
  end: 31 August 2018
  description:
    <a href="http://flippac.org/">Philippa Cowderoy</a> visiting.


- date: 9 August 2018
  description:
    <a href="http://www.cs.ubc.ca/~rxg/">Ron Garcia</a> visiting.


- start: 16 July 2018
  end: 20 July 2018
  description:
    <a href="http://jurriaan.me/">Jurriaan Rot</a> visiting.


- date: 28 May 2018
  description:
    <a href="http://ashinkarov.github.io/">Artem Shinkarov</a>
    visiting.


- start: 14 May 2018
  end: 30 May 2018
  description:
    <a href="http://homepage.tudelft.nl/c9d1n/">Helle Hvid Hansen</a>
    visiting.



- start: 27 March 2018
  end: 28 March 2018
  description:
    <a href="http://www.cs.nott.ac.uk/~txa/">Thorsten Altenkirch</a> visiting.


- date: 21 March 2018
  description:
    <a href="http://www.gabbay.org.uk/">Jamie Gabbay</a> visiting.


- date: 7 February 2018
  description:
    <a href="https://justinh.su/">Justin Hsu</a> visiting.


- start: 22 January 2018
  end: 26 January 2018
  description:
    <a href="http://jurriaan.me/">Jurriaan Rot</a> visiting.

- date: 6 December 2017
  description:
    <a href="http://sf.snu.ac.kr/gil.hur/">Chung-Kil Hur</a> visiting.


- start: 23 October 2017
  end: 27 October 2017
  description:
    <a href="http://johannesmarti.com/">Johannes Marti</a> visiting.


- date: 11 September 2017
  description:
    <a href="https://saizan.github.io/">Andrea Vezzosi</a> visiting.


- date: 27 July 2017
  description:
    <a href="https://sites.google.com/site/researchcavaliere/">Matteo Cavaliere</a> visiting.


- start: 10 July 2017
  end: 11 July 2017
  description:
    We are organising a <a href="/opengames-2017/">Workshop on Open Games</a>.


- date: 5 July 2017
  description:
    <a href="http://noamz.org/">Noam Zeilberger</a> visiting.


- date: 30 June 2017
  description:
    <a href="https://danelahman.github.io/">Danel Ahman</a> visiting.


- start: 26 June 2017
  end: 30 June 2017
  description:
    Stephan Spahn visiting.


- start: 10 April 2017
  end: 12 April 2017
  description:
    We are organising the eighth edition of the workshop <a href='https://personal.cis.strath.ac.uk/clemens.kupke/ALCOP2017/'>Algebra and Coalgebra meet Proof Theory</a>.


- date: 6 February 2017
  description:
    <a href='http://www.cs.ox.ac.uk/people/ohad.kammar/main.html'>Ohad
    Kammar</a> visiting.

- date: 30 November 2016
  description:
    We are organising the second meeting  <a href='http://homepages.inf.ed.ac.uk/cheunen/clapscotland/'>Categories, Logic, and Physics, Scotland</a>.


- start: 21 November 2016
  end: 25 November 2016
  description:
    <a href='https://staff.science.uva.nl/y.venema/'>Yde Venema</a>
    and <a href="http://homepage.tudelft.nl/c9d1n/">Helle Hvid Hansen</a>
    visiting.


- date: 9 November 2016
  description:
    We are organising a meeting of the <a href='https://msp-strath.github.io/spls-16/'>Scottish Programming Languages Seminar</a>.


- date: 3 October 2016
  description:
    Welcome to Alasdair Lambert and Simone Barlocco who are starting
    PhDs in the MSP group.


- start: 15 September 2016
  end: 16 September 2016
  description:
    <a href="http://www.cs.ox.ac.uk/people/julian.hedges/home.html">Jules Hedges</a> visiting.


- date: 12 September 2016
  description:
    "Congratulations to Federico Orsanigo for successfully defending his thesis &quot;Bifibrational parametricity: from zero to two dimensions&quot;!"

- start: 12 September 2016
  end: 13 September 2016
  description:
    <a href='https://www.fmf.uni-lj.si/si/imenik/32646/'>Alex Simpson</a> visiting.


- start: 5 September 2016
  end: 9 September 2016
  description:
    Stephan Spahn visiting.


- start: 20 April 2016
  end: 26 April 2016
  description:
    We are organising the 33rd <a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXXIII">Agda Implementors’ Meeting</a> at Strathclyde.


- start: 29 February 2016
  end: 2 March 2016
  description:
    Stephan Spahn visiting.


- date: 26 January 2016
  description:
    <a href="http://www.cs.ru.nl/A.Kissinger/">Aleks Kissinger</a> visiting.


- start: 25 January 2016
  end: 29 January 2016
  description:
    <a href="http://www.bath.ac.uk/comp-sci/contacts/academics/john_power/">John Power</a> visiting.

- date: 18 November 2015
  description:
    <a href="http://bram.westerbaan.name/home">Bram Westerbaan</a> visiting.


- start: 19 October 2015
  end: 23 October 2015
  description:
    <a href="http://www.vikwin.de/">Viktor Winschel</a> visiting.


- start: 5 October 2015
  end: 9 October 2015
  description:
    <a href="http://www.appliedlogictudelft.nl/alessandra-palmigiano/">Alessandra Palmigiano</a> visiting.


- date: 30 September 2015
  description:
    Welcome to Ben Price who is starting a PhD under the supervision
    of Neil Ghani.



- start: 23 September 2015
  end: 25 September 2015
  description:
    <a href="http://perso.ens-lyon.fr/pierre.lescanne/">Pierre Lescanne</a> visiting.


- start: 14 September 2015
  end: 18 September 2015
  description:
   <a href='https://sites.google.com/site/homepagegcina/'>Giovanni Cina</a> visiting.


- start: 25 August 2015
  end: 29 August 2015
  description:
    <a href="http://www.eecs.qmul.ac.uk/~julesh/">Julian Hedges</a> visiting.


- date: 13 August 2015
  description:
    <a href="http://wphomes.soic.indiana.edu/jsiek/">Jeremy Siek</a> visiting.

- start: 25 May 2015
  end: 27 May 2015
  description:
    <a href="http://www.cs.bham.ac.uk/~pbl/">Paul Levy</a> visiting.


- date: 20 March 2015
  description:
    <a href="http://www.cs.ox.ac.uk/people/chris.heunen/">Chris Heunen</a> visiting.

- date: 4 March 2015
  description:
    We are organising <a href="hott-afternoon/">A HoTT-Date with Thorsten Altenkirch</a> &mdash; an afternoon of talks.


- start: 2 March 2015
  end: 6 March 2015
  description:
    <a href="http://www.cs.nott.ac.uk/~txa/">Thorsten Altenkirch</a> visiting.

- start: 20 January 2015
  end: 23 January 2015
  description:
    <a href="http://cs.ioc.ee/~james/">James Chapman</a> visiting.

- start: 9 December 2014
  end: 10 December 2014
  description:
    <a href="http://www.cs.ox.ac.uk/people/aleks.kissinger/about.html">Aleks Kissinger</a> visiting.



- start: 26 September 2014
  end: 3 October 2014
  description:
    <a href="http://www.cs.ru.nl/~helle/">Helle Hvid Hansen</a> visiting.


- date: 30 September 2014
  description:
    Welcome to Kevin Dunne who is starting a PhD under the supervision
    of Ross Duncan.


- start: 23 June 2014
  end: 24 June 2014
  description:
    "<a id='fibs2014'></a>Upcoming event: <a href='fibs-2014/'>Workshop on Fibrations in Computer Science</a> organised at Strathclyde."


- start: 4 June 2014
  end: 6 June 2014
  description:
    The SICSA theme event
    <a href="http://staff.computing.dundee.ac.uk/katya/practical-types/">Practical Types</a>
    is organised by Neil and others, and attended by many of the MSP group.




- start: 28 May 2014
  end: 29 May 2014
  description:
    <a href="http://www.cl.cam.ac.uk/~ok259/">Ohad Kammar</a> visiting.


- date: 22 May 2014
  description:
    <a href="http://homepages.inf.ed.ac.uk/s1225336/hott-reading-group/">Homotopy Type Theory reading group</a> session on Higher Inductive Types will meet at Strathclyde.


- date: 15 April 2014
  description:
    <p><a href="http://www0.cs.ucl.ac.uk/staff/J.Brotherston/">James Brotherston</a> visiting and giving a talk in the Departmental seminar at 3pm in room LT14.15 about <em>Parametric completeness for separation theories (via hybrid logic)</em>.</p>
    <p><strong>Abstract:</strong> In this talk, we consider the logical gap between the following two concepts:</p>
    <p>(1) provability in a propositional axiomatisation of separation logic, which is usually given by the bunched logic BBI; and</p>
    <p>(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.</p>
    <p>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).</p>
    <p>This is joint work with <a href="http://www.doc.ic.ac.uk/~jvillar1/">Jules Villard</a>, now at Imperial.</p>


- date: 9 April 2014
  description:
    <p>
    <a href="http://homepages.inf.ed.ac.uk/da/">David Aspinall</a> visiting and giving a talk in the Departmental seminar about <em>Managing Proofs Hierarchically</em>.
    </p>
    <p>
      <strong>Abstract:</strong> 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.
    </p>


- date: 7 April 2014
  description:
    <a href="http://www.gabbay.org.uk/">Jamie Gabbay</a> visiting.

- start: 31 March 2014
  end: 4 April 2014
  description:
    <a href="http://www.cs.nott.ac.uk/~txa/">Thorsten Altenkirch</a> visiting.

- date: 16 August 2013
  description:
    <a id="RobinAdams"></a> 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.


- date: 12 August 2013
  description:
    <a id="andygill"></a> Neil Ghani has been awarded a SICSA Distinguished
    Fellowship to host <a href="http://www.ittc.ku.edu/csdl/fpg/users/andygill.html">Andy Gill</a> 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.

- date: 4 August 2013
  description:
    <a id="cmuanu"></a> 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!

- date: 29 July 2013
  description:

    <a id="lecturer2"></a> We are currently looking for a new <a href
    = "http://www.mis.strath.ac.uk/Personnel/open/1432013.pdf">
    Lecturer or Senior Lecturer </a> within the MSP group. See the
    above link for how to apply (deadline is 8 September
    2013). Ideally we are looking for someone who
    <ul>
      <li> 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) </li>
      <li> Offers us something new and exciting that we ought to have some strength in but don't. </li>
      <li> 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. </li>
    </ul>

- date: 23 July 2013
  description:
    <a id="AlwinBlock"></a> Alwin Blok will be joining the MSP group
    to study for a PhD under Clemens expert supervision.


- date: 23 May 2013
  description:
    <a id="fred"></a> 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!


- date: 22 May 2013
  description:
    <a id="parametricity2013"></a>Patricia Johann is organising this year's <a href="http://www.msp.cis.strath.ac.uk/parametricity-2013/">Parametricity Workshop</a> at Strathclyde.

- date: 1 January 2013
  description:
    <a id="lecturer"></a><a href="http://www.cs.ox.ac.uk/people/clemens.kupke/">Clemens
    Kupke</a> has taken up a lectureship position within the
    group.

- date: 3 October 2012
  description:
    <a id="students2012"></a>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.


- date: 15 June 2012
  description:
    <a id="lectureship"><strong>Lectureship in the Mathematically Structured Programming Group</strong></a>

    <p>
      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.

    <p>
      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.

    <p>
      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 <a href="http://www.mis.strath.ac.uk/Personnel/open/712012.pdf">http://www.mis.strath.ac.uk/Personnel/open/712012.pdf</a>.

    <p>
      The closing date for applications is Thursday July 26.


- date: 15 June 2012
  description:
    "<a id='lambda2012'></a>Upcoming event: <a href='lambda2012/'>International Workshop on 75 Years of the λ-Calculus</a>"


- date: 1 June 2012
  description:
    <a id='clem'></a>Congratulations to Clement Fumex on passing his
    viva! Clement's thesis is entitled &quot;Induction and Coinduction
    schemes in Category Theory&quot;. His examiners
    were <a href='http://www.cs.ru.nl/~bart/'>Bart Jacobs</a>
    (external) and
    <a href='https://personal.cis.strath.ac.uk/conor.mcbride/'>Conor
    McBride</a> (internal). Clement's thesis was supervised by <a
    href='https://personal.cis.strath.ac.uk/patricia.johann/'>Patty
    Johann</a>.


- date: 25 May 2012
  description:
    "<a id='scotcats-25may2012'></a>Upcoming event: <a href='https://personal.cis.strath.ac.uk/~ng/SCT/sct250512.html'>6th Scottish Category Theory Seminar</a>."

- date: 2 May 2012
  description:
    "<a id='para-2012'></a>Event <a href='parametricity-2012'>Parametricity Workshop</a>."


- date: 7 March 2012
  description:
    "<a id='phd-07mar2012'></a><strong>PhD Position: Higher Dimensional Categories and Types</strong><p>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.  </p><p>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.  </p><p>Anyone interested should in the first instance contact Professor Neil Ghani whose email address is &quot;ng at cis.strath.ac.uk&quot; and outline their academic background. Applications will be considered on a first come, first served basis.</p>"


- date: 10 February 2012
  description:
    <a id="stp-feb-2012"></a><a href="stp-feb-2012/">Scottish Theorem Provers Meeting</a>

- date: 19 December 2011
  description:
    <a id="hank60"></a><a href="hank60/index.html">Peter Hancock at 60</a>

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

    <p>
      <a href="hank60/index.html">More information</a>.


- date: 25 November 2011
  description:
    <a id="sct5"></a><a href="http://homepages.inf.ed.ac.uk/als/SCT/sct111125.html">5th Scottish Category Theory Seminar</a>


- date: 16 August 2011
  description:
     <a id='6monthpostdoc'></a><strong>6 Month Postdoc Position</strong> <p> Mathematically Structured Programming Group<br/> University of Strathclyde<br/> Scotland<br/> <p> 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.  <p> 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.  <p> The candidate we are looking for should be highly self motivated and appreciate that without beauty, we are lost.  <p> 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.  <p> For more information, please contact <p> Professor Neil Ghani<br/> <a href='mailto:ng@cis.strath.ac.uk'>ng@cis.strath.ac.uk</a><br/> <a href='http://personal.cis.strath.ac.uk/~ng/'>http://personal.cis.strath.ac.uk/~ng/</a><br/> <a href='http://msp.cis.strath.ac.uk/'>http://msp.cis.strath.ac.uk/</a><br/>


- date: 4 August 2011
  description:
    "<a id='panangaden-20110804'></a><a href='http://www.cs.mcgill.ca/~prakash/'>Prakash Panangaden</a> talk. 2pm.<p><strong>Title:</strong> The Duality of State and Observation</p><p><em>Abstract:</em> 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.</p>"


- start: 1 June 2011
  end: 2 June 2011
  description:
    <a href="http://www.cs.ru.nl/~bart/">Bart Jacobs</a> visited.


- date: 17 May 2011
  description:
    "<a id='scott-20110517'></a><a href='http://www.site.uottawa.ca/~phil/'>Phil Scott</a> talk.<p><strong>Title:</strong> Traced categories: algebraic structure of feedback and partial feedback in networks<p><em>Abstract:</em> 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 &quot;traced monoidal category&quot;, 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."


- date: 13 May 2011
  description:
    <a href="http://www.maths.gla.ac.uk/~tl/sct110513.html">4th Scottish Category Theory Seminar</a>


- start: 21 April 2011
  end: 25 April 2011
  description:
    <a href="http://www.iai.uni-bonn.de/~jv/">Janis Voigtländer</a> visited.


- date: 17 February 2011
  description:
    <a id="gambino-20110217"></a><a href="http://www.math.unipa.it/~ngambino/">Nicola Gambino</a> talk. 12pm. Location 14.15.

    <p>
      <strong>Title:</strong> Voevodsky's Univalence Axiom

    <p>
      <em>Abstract:</em> 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.

- date: 3 December 2010
  description:
    "<a href='http://personal.cis.strath.ac.uk/~ng/SCT/sct021210.html'>Algebraic Set Theory Course: Benno van den Berg</a>"


- date: 2 December 2010
  description:
    <a href="http://personal.cis.strath.ac.uk/~ng/SCT/sct021210.html">3rd Scottish Category Theory Seminar</a>


- start: 22 November 2010
  end: 26 November 2010
  description:
    <a href="http://www.cs.ru.nl/~wouters/">Wouter Swierstra</a> visiting.


- date: 24 November 2010
  description:
    <a href="http://www.dcs.gla.ac.uk/research/spls/Nov10/index.html">Scottish Programming Languages Seminar</a>