msp101-old.html

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

<h2>MSP101</h2>

<p>MSP101 is an ongoing series of informal talks given on Wednesday
mornings by visiting academics or members of the MSP group. They are
usually announced on the
<a href="https://lists.cis.strath.ac.uk/mailman/listinfo/msp-interest">
msp-interest</a> mailing-list.</p>

<!--<h2>Upcoming talks</h2>-->

<h2>List of previous talks</h2>

<dl>
  <dt>2014-05-28: Graphical algebraic foundations for monad stacks (<a href="http://www.cl.cam.ac.uk/~ok259/">O. Kammar<a/>)</dt>
  <dd>
    <p>
      Ohad gave an informal overview of his current draft, with the
      following abstract:
    </p><p>
      Haskell incorporates computational effects modularly using
      sequences of monad transformers, termed monad stacks. The
      current practice is to find the appropriate stack for a given
      task using intractable brute force and heuristics. By
      restricting attention to algebraic stack combinations, we
      provide a linear-time algorithm for generating all the
      appropriate monad stacks, or decide no such stacks exist. Our
      approach is based on Hyland, Plotkin, and Power’s algebraic
      analysis of monad transformers, who propose a graph-theoretical
      solution to this problem. We extend their analysis with a
      straightforward connection to the modular decomposition of a
      graph and to cographs, a.k.a. series-parallel graphs.
    </p><p>
      We present an accessible and self-contained account of this
      monad-stack generation problem, and, more generally, of the
      decomposition of a combined algebraic theory into sums and
      tensors, and its algorithmic solution. We provide a web-tool
      implementing this algorithm intended for semantic investigations
      of effect combinations and for monad stack generation.
    </p> 
  </dd>
</dl>

<dl>
<dt>2014-05-21: Coalgebraic Foundations of Databases (C. Kupke)</dt>
  <dd>
    This 101 is intended to be a brainstorming session on possible
    links between the theory of coalgebras and the theory of
    databases.  I will outline some ideas in this direction and I am
    looking forward to your feedback.
  </dd>
</dl>

<dl>
<dt>2014-05-14: Resource aware contexts and proof search for IMLL (G. Allais)</dt>
  <dd>
  <p>In Intuitionistic Multiplicative Linear Logic, the right
  introduction rule for tensors implies picking a 2-partition of the
  set of assumptions and use each component to inhabit the
  corresponding tensor's subformulas. This makes a naïve proof search
  algorithm intractable.  Building a notion of resource availability
  in the context and massaging the calculus into a more general one
  handling both resource consumption and a notion of "leftovers" of a
  subproof allows for a well-structured well-typed by construction
  proof search mechanism.</p>
  
  <p>Here is an <a href="http://gallais.org/code/LinearProofSearch/poc.LinearProofSearch.html">Agda file</a> implementing the proof search algorithm.</p>
  </dd>
</dl>

<dl>
  <dt>2014-04-07: Nominal sets (<a href="http://www.gabbay.org.uk/">J. Gabbay<a/>)</dt>
</dl>

<dl>
<dt>2014-04-02: Towards cubical type theory (<a href="http://www.cs.nott.ac.uk/~txa/">T. Altenkirch<a/>)</dt>
</dl>

<dl>
<dt>2014-03-19: The selection monad transformer (G. Allais)</dt>
  <dd>
  Guillaume presented parts of Hedges' paper <a href="http://www.eecs.qmul.ac.uk/~julesh/papers/monad_transformers.pdf">Monad
    transformers for backtracking search</a> (accepted
    to <a href="http://www.cs.bham.ac.uk/~pbl/msfp2014/">MSFP
    2014</a>). The paper extends Escardo and Oliva's work on the
    selection and continuation monads to the corresponding monad
    transformers, with applications to backtracking search and game
    theory.
  </dd>
</dl>

<dl>
  <dt>2014-03-05, 3pm: Lagrange Inversion (S. Hannah)</dt>
  <dd>
    Stuart spoke about Lagrange inversion, a species-theoretic attempt to discuss the existence of solutions to equations defining species.
  </dd>
</dl>

<dl>
  <dt>2014-02-28, 2pm: Species (N. Ghani)</dt>
  <dd>
    Neil spoke about how adding structured quotients to containers
    gives rise to a larger class of data types.
  </dd>
</dl>

<dl>
  <dt>2014-02-19: Synthetic Differential Geometry (T. Revell)</dt>
  <dd>
    Tim gave a brief introduction to Synthetic Differential
    Geometry. This is an attempt to treat smooth spaces categorically
    so we can extend the categorical methods used in the discrete
    world of computer science to the continuous work of physics.
  </dd>
</dl>

<dl>
  <dt>2014-02-12: Worlds (C. McBride)</dt>
  <dd>
    Conor talked about worlds (aka phases, aka times, ...): why one
    might bother, and how we might go about equipping type theory with
    a generic notion of permitted information flow.
  </dd>
</dl>

<dl>
  <dt>2014-02-05: Operads (M. Gould)</dt>
  <dd>
    Miles Gould has kindly agreed to come through and tell us about
    Operads, thus revisiting the topic of his PhD and the city in
    which he did it.
  </dd>
</dl>

<dl>
  <dt>2014-01-22: Overview of (extensions of) inductive-recursive definitions (L. Malatesta)</dt>
  <dd>
  </dd>

  <dt>2014-01-08: On the recently found inconsistency of the
  univalence axiom in current Agda and Coq (C. McBride)</dt>
  <dd>
  </dd>

  <dt>2013-12-18: Quantum Mechanics (R. Duncan)</dt>
  <dd>
  </dd>

  <dt>2013-11-20: Classical Type Theories (R. Adams)</dt>
  <dd>
    In 1987, Felleisen showed how to add control operators (for things like
    exceptions and unconditional jumps) to the untyped lambda-calculus.  In
    1990, Griffin idly wondered what would happen if one did the same in a
    typed lambda calculus.  The answer came out: the inhabited types become
    the theorems of classical logic.<br />

    I will present the lambda mu-calculus, one of the cleanest attempts to
    add control operators to a type theory.  We'll cover the good news: the
    inhabited types are the tautologies of minimal classical logic, and Godel's
    Double Negation translation from classical to intuitionistic logic turns
    into the CPS translation.<br />

    And the bad news: control operators don't play well with other types. Add
    natural numbers (or some other inductive type), and you get inconsistency.
    Add Sigma-types, and you get degeneracy (any two objects of the same type
    are definitionally equal).  It gets worse: add plus-types, and you break
    Subject Reduction.
  </dd>

  <dt>2013-11-13: Continuation Passing Style (G. Allais)</dt>
  <dd>
    I chose to go through (parts of) Hatcliff and Danvy's paper
    <a href="http://dl.acm.org/citation.cfm?id=178053">
    "A Generic Account of Continuation-Passing Styles"</a> (POPL 94)
    which gives a nice factorization of various CPS transforms in
    terms of:
    <ul>
      <li>embeddings from STLC to Moggi's computational meta-language
          (either call-by-value, call-by-name, or whatever you can come
          up with)</li>
      <li>followed by a generic CPS transform transporting terms from ML
          back to STLC</li>
    </ul>

   Here is <a href="http://gallais.org/code/GenericCPS/definitions.html">an Agda
   file</a> containing what we had the time to see.
  </dd>
</dl>