old-news.html

### default.html(section.news=current)

<h2>Older News</h2>

<h3>2015</h3>

<dl>
  <dt>25 &ndash; 27 May 2015</dt>
  <dd>
    <a href="http://www.cs.bham.ac.uk/~pbl/">Paul Levy</a> visiting.
  </dd>

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

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

  
  <dt>2 &ndash; 6 March 2015</dt>
  <dd>
    <a href="http://www.cs.nott.ac.uk/~txa/">Thorsten Altenkirch</a> visiting.
  </dd>

  <dt>20 &ndash; 23 January 2015</dt>
  <dd>
    <a href="http://cs.ioc.ee/~james/">James Chapman</a> visiting.
  </dd>
</dl>

<h3>2014</h3>

<dl>
  <dt>9 &ndash; 10 December 2014</dt>
  <dd>
    <a href="http://www.cs.ox.ac.uk/people/aleks.kissinger/about.html">Aleks Kissinger</a> visiting.
  </dd>


  <dt>26 September &ndash; 3 October 2014</dt>
  <dd>
    <a href="http://www.cs.ru.nl/~helle/">Helle Hvid Hansen</a> visiting.
  </dd>

  <dt>30 September 2014</dt>
  <dd>
    Welcome to Kevin Dunne who is starting a PhD under the supervision
    of Ross Duncan.
  </dd>

  <dt>23 &ndash; 24 June 2014</dt>
  <dd>
    <a id="fibs2014"></a>Upcoming event: <a href="fibs-2014/">Workshop on Fibrations in Computer Science</a> organised at Strathclyde.
  </dd>

  <dt>4 &ndash; 6 June 2014</dt>
  <dd>
    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.
  </dd>



  <dt>28 &ndash; 29 May 2014</dt>
  <dd>
    <a href="http://www.cl.cam.ac.uk/~ok259/">Ohad Kammar</a> visiting.
  </dd>

  <dt>22 May 2014</dt>
  <dd>
    <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.
  </dd>

  <dt>15 April 2014</dt>
  <dd>
    <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>
  </dd>

  <dt>9 April 2014</dt>
  <dd>
    <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>
  </dd>


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

  <dt>31 March &ndash; 4 April 2014</dt>
  <dd>
    <a href="http://www.cs.nott.ac.uk/~txa/">Thorsten Altenkirch</a> visiting.
  </dd>


</dl>

<h3>2013</h3>

<dl>

  <dt>16 August 2013</dt>
  <dd><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.
  </dd>


  <dt>12 August 2013</dt>
  <dd><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.
  </dd>


  <dt>4 August 2013</dt>
  <dd><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!
 </dd>


  <dt>29 July 2013</dt>
  <dd><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>
</dd>


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


  <dt>23 May 2013</dt>
  <dd><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!
  </dd>

  <dt>22 May 2013</dt>
  <dd><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.
    </dd>
  <dt>1 January 2013</dt>
  <dd>
    <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.
  </dd>

</dl>

<h3>2012</h3>

<dl>
  <dt>3 October 2012</dt>
  <dd>
    <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.
  </dd>

  <dt>15 June 2012</dt>
  <dd>
    <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.
  </dd>

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

  <dt>1 June 2012</dt>
  <dd>
    <a id="clem"></a>Congratulations to Clement Fumex on passing his
    viva! Clement's thesis is entitled "Induction and Coinduction
    schemes in Category Theory". 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>.
  </dd>

  <dt>25 May 2012</dt>
  <dd>
    <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>.
  </dd>


  <dt>2 May 2012</dt>
  <dd>
    <a id="para-2012"></a>Event: <a href="parametricity-2012">Parametricity Workshop</a>
  </dd>

  <dt>7 March 2012</dt>
  <dd>
    <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>
      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>
      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.
  </dd>

  <dt>10 February 2012</dt>
  <dd>
    <a id="stp-feb-2012"></a><a href="stp-feb-2012/">Scottish Theorem Provers Meeting</a>
  </dd>
</dl>

<h3>2011</h3>

<dl>
  <dt>19 December 2011</dt>
  <dd>
    <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>.
  </dd>

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

  <dt>16 August 2011</dt>
  <dd>
    <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/>
  </dd>

  <dt>4th August 2011</dt>
  <dd>
    <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>
      <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.
  </dd>

  <dt>1 &ndash; 2 June 2011</dt>
  <dd>
    <a href="http://www.cs.ru.nl/~bart/">Bart Jacobs</a> visited.
  </dd>

  <dt>17 May 2011</dt>
  <dd>
    <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
      "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.
  </dd>

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

  <dt>21 &ndash; 25 April 2011</dt>
  <dd>
    <a href="http://www.iai.uni-bonn.de/~jv/">Janis Voigtländer</a> visited.
  </dd>

  <dt>17 February 2011</dt>
  <dd>
    <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.
  </dd>
</dl>

<h3>2010</h3>

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

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

  <dt>22 &ndash; 26 November 2010</dt>
  <dd>
    <a href="http://www.cs.ru.nl/~wouters/">Wouter Swierstra</a> visiting.
  </dd>

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