diff --git a/.github/workflows/generate-website.yml b/.github/workflows/generate-website.yml index 417abc8..c0cb08d 100644 --- a/.github/workflows/generate-website.yml +++ b/.github/workflows/generate-website.yml @@ -59,6 +59,9 @@ jobs: - name: Generate 101 run: Generate101 + - name: Generate News + run: GenerateNews + - name: Generate website run: Generate diff --git a/Generate.hs b/Generate.hs index ece2079..f5e6aeb 100644 --- a/Generate.hs +++ b/Generate.hs @@ -126,7 +126,7 @@ substitute template env = loop template [] let varNm = reverse varAcc in case lookup varNm env of Nothing -> loop cs acc - Just val -> loop cs (reverse val ++ acc) + Just val -> loop cs (reverse (substitute val env) ++ acc) getVar (c:cs) varAcc acc = getVar cs (c:varAcc) acc -- | Check the input string to determine if it starts with a header of diff --git a/GenerateNews.hs b/GenerateNews.hs new file mode 100644 index 0000000..1b7daff --- /dev/null +++ b/GenerateNews.hs @@ -0,0 +1,151 @@ +{-# LANGUAGE DeriveGeneric, OverloadedStrings #-} +module Main where + +import Prelude hiding (div) +import GHC.Generics +import Data.Yaml + +import Data.List +import Data.Maybe +import Data.Function + +-- import Data.ByteString.Lazy (ByteString) +-- import qualified Data.ByteString.Lazy as LBS +import qualified Data.ByteString as BS +import Data.Text (Text) +import qualified Data.Text as T + +import Control.Applicative + +import Network.HTTP.Client +import Network.HTTP.Client.TLS +import Network.HTTP.Types.Status + +import Data.Time +import Data.Time.Format + +import Text.Feed.Types +import Text.Feed.Import +import Text.Feed.Query + +import Html + +------------------------------------------------------------------------------ +-- number of days to cut off old news +oldCutoff :: Integer +oldCutoff = 365 * 5 +------------------------------------------------------------------------------ + + +data NewsDate + = OneDate Day + | DateRange Day Day + deriving (Show, Eq) + +startDate :: NewsDate -> Day +startDate (OneDate d) = d +startDate (DateRange s e) = s + +newsDateToHTML :: NewsDate -> HTML +newsDateToHTML (OneDate day) = formatTime defaultTimeLocale "%e %B %Y" day +newsDateToHTML (DateRange start end) = + let (sy, sm, sd) = toGregorian start + (ey, em, ed) = toGregorian end + wholeMonths = sd == 1 && ed == gregorianMonthLength ey em + in case (sy == ey, sm == em, sd == ed, wholeMonths) of + (True, True, True, _) -> newsDateToHTML (OneDate start) + (True, True, False, True) -> fmt "%B %Y" end + (True, True, False, False) -> fmt "%e" start ++ dash ++ fmt "%e %B %Y" end + (True, False, False, True) -> fmt "%B" start ++ dash ++ fmt "%B %Y" end + (True, False, False, False) -> fmt "%e %B" start ++ dash ++ fmt "%e %B %Y" end + (_, _, _, True) -> fmt "%B %Y" start ++ dash ++ fmt "%B %Y" end + _ -> fmt "%e %B %Y" start ++ dash ++ fmt "%e %B %Y" end + where fmt = formatTime defaultTimeLocale + dash = " – " + +instance Ord NewsDate where + compare = compare `on` startDate + +data News = News + { date :: NewsDate + , desc :: String + } + deriving (Show, Eq) + +instance FromJSON News where + parseJSON = withObject "News" $ \ v -> do + desc <- v .: "description" + date <- single v <|> range v + pure (News date desc) + where + single v = do + date <- v .: "date" >>= parseTimeM True defaultTimeLocale "%e %B %Y" + pure (OneDate date) + range v = do + start <- v .: "start" >>= parseTimeM True defaultTimeLocale "%e %B %Y" + end <- v .: "end" >>= parseTimeM True defaultTimeLocale "%e %B %Y" + pure (DateRange start end) + + +newsToHTML :: News -> HTML +newsToHTML n = ddt (newsDateToHTML (date n), desc n) + +generateNews :: FilePath -> IO (HTML -- current news + , [(Year, HTML)] -- old news, grouped by year + ) +generateNews file = do + now <- getCurrentTime + f <- BS.readFile file + case decodeEither' f of + Left err -> + error (show err) + Right news -> do + let (old, new) = partition (\ x -> date x < OneDate (addDays (-oldCutoff) (utctDay now))) news + let oldGrouped = groupBy (\ a b -> startYear a == startYear b) old + pure (dlist new, map (\ x -> (startYear (head x), dlist x)) oldGrouped) + where + startYear x = let (y,_,_) = toGregorian (startDate (date x)) in y + dlist [] = "" + dlist x = tag "dl" (unlines (map newsToHTML x)) + +------------------------------------------------------------------------------ +pubsRSS :: Request +pubsRSS = parseRequest_ "https://pureportal.strath.ac.uk/en/organisations/mathematically-structured-programming/publications/?format=rss" + +getPureRSS :: Int -- number of entries + -> IO [Item] +getPureRSS n = do + manager <- newManager tlsManagerSettings + res <- httpLbs pubsRSS manager + case statusIsSuccessful (responseStatus res) of + False -> pure [] + True -> do + case parseFeedSource (responseBody res) of + Nothing -> pure [] + Just feed -> pure $ take n $ reverse $ sortOn (getItemPublishDate :: Item -> Maybe (Maybe UTCTime)) (feedItems feed) + + +itemToHTML :: Item -> Maybe HTML +itemToHTML i = do + -- title <- T.unpack <$> getItemTitle i + -- link <- T.unpack <$> getItemLink i + -- title and link are included in the description + desc <- T.unpack <$> getItemDescription i + pure desc + +main :: IO () +main = do + + rss <- getPureRSS 5 + let header = "### default.html(section.news=current,headtags=)\n" + let items = catMaybes $ map itemToHTML rss + let pubs = if (null items) then "" else + div "recent-pubs" $ + (h2 "Recent MSP publications") ++ + (ulist items) ++ + p ("See the " ++ (anchor "https://pureportal.strath.ac.uk/en/organisations/mathematically-structured-programming" "MSP PURE page") ++ " for a full list of recent papers, grants, etc.") + (newNews, oldNews) <- generateNews "_news.yaml" + let news = h2 "News" ++ newNews ++ if null oldNews then "" else h3 "Older News" ++ p ("See here for " ++ anchor "old-news.html" "older news" ++ ".") + let oldPage = h2 "Older news" ++ concatMap (\ (y, ds) -> h3 (show y) ++ ds) oldNews + writeFile "news.html" (header ++ pubs ++ news) + if null oldNews then pure () else writeFile "old-news.html" (header ++ oldPage) diff --git a/GeneratePeople.hs b/GeneratePeople.hs index d7c804f..d834005 100644 --- a/GeneratePeople.hs +++ b/GeneratePeople.hs @@ -6,6 +6,8 @@ import GHC.Generics import Data.Yaml import qualified Data.ByteString as BS +import Html + type Markdown = String data Status = Academic | PhDStudent | Research | PhDFinished | Alum @@ -22,15 +24,14 @@ instance FromJSON Status where data LinkRelationship = HomePage - | Staff | Pure | Thesis - | Uni + | Staff deriving (Show, Eq, Generic) instance FromJSON LinkRelationship where parseJSON (String "homepage") = pure HomePage - parseJSON (String "uni") = pure Uni + parseJSON (String "staff") = pure Staff parseJSON (String "pure") = pure Pure parseJSON (String "thesis") = pure Thesis parseJSON _ = fail "invalid link type" @@ -61,38 +62,14 @@ data Person = Person instance FromJSON Person ------------------------------------------------------------------------------ -type HTML = String - -div :: String -> HTML -> HTML -div klass content = - "
" ++ content ++ "
" - -h5 :: HTML -> HTML -h5 content = "
" ++ content ++ "
" - -p :: HTML -> HTML -p content = "

" ++ content ++ "

" - -ulist :: [HTML] -> HTML -ulist items = "" - -anchor :: String -> HTML -> HTML -anchor url content = "" ++ content ++ "" - -img :: String -> HTML -img url = "" linkToHTML :: Link -> HTML linkToHTML link = case rel link of HomePage -> anchor (href link) "homepage" - Uni -> anchor (href link) "Staff page" + Staff -> anchor (href link) "Staff page" Pure -> anchor (href link) "Staff page (pure)" Thesis -> anchor (href link) "PhD Thesis" -emailToHTML :: String -> HTML -emailToHTML emailAddr = - anchor ("mailto:" ++ emailAddr) ("Email: " ++ emailAddr) - statusToHTML :: Status -> HTML statusToHTML Academic = "Academic staff" statusToHTML Research = "Research staff" diff --git a/Html.hs b/Html.hs new file mode 100644 index 0000000..292384a --- /dev/null +++ b/Html.hs @@ -0,0 +1,42 @@ +module Html where + +type HTML = String + +tag :: String -> HTML -> HTML +tag t content = "<" ++ t ++ ">" ++ content ++ "" + +div :: String -> HTML -> HTML +div klass content = + "
" ++ content ++ "
" + +hn :: Int -> HTML -> HTML +hn n = tag ("h" ++ show n) + +h5 :: HTML -> HTML +h5 = hn 5 + +h3 :: HTML -> HTML +h3 = hn 3 + +h2 :: HTML -> HTML +h2 = hn 2 + +p :: HTML -> HTML +p = tag "p" + +ulist :: [HTML] -> HTML +ulist items = "" + + +ddt :: (HTML, HTML) -> HTML +ddt (term, desc) = "
" ++ term ++ "
" ++ desc ++ "
" + +anchor :: String -> HTML -> HTML +anchor url content = "" ++ content ++ "" + +img :: String -> HTML +img url = "" + +emailToHTML :: String -> HTML +emailToHTML emailAddr = + anchor ("mailto:" ++ emailAddr) ("Email: " ++ emailAddr) diff --git a/MSPweb.cabal b/MSPweb.cabal index bdb91c7..f081692 100644 --- a/MSPweb.cabal +++ b/MSPweb.cabal @@ -34,7 +34,22 @@ executable Generate101 executable GeneratePeople main-is: GeneratePeople.hs + other-modules: Html build-depends: base, yaml, bytestring default-language: Haskell2010 + +executable GenerateNews + main-is: GenerateNews.hs + other-modules: Html + build-depends: base, + yaml, + bytestring, + http-client, + http-client-tls, + http-types, + time, + feed, + text + default-language: Haskell2010 diff --git a/Makefile b/Makefile index 37909be..17f66f2 100644 --- a/Makefile +++ b/Makefile @@ -32,6 +32,7 @@ default: local local: runghc Generate101.hs + runghc GenerateNews.hs runghc Generate.hs compile: @@ -39,6 +40,7 @@ compile: local-compiled: `cabal list-bin --builddir _dist Generate101` + `cabal list-bin --builddir _dist GenerateNews` `cabal list-bin --builddir _dist Generate` diff --git a/_news.yaml b/_news.yaml new file mode 100644 index 0000000..3ab2f47 --- /dev/null +++ b/_news.yaml @@ -0,0 +1,735 @@ +- date: 5 May 2023 + description: + Welcome to Iwan Quémerais, who is doing an internship with + Clemens Kupke over the summer. + +- date: 5 May 2023 + description: + Johannes Marti visiting. + +- date: 4 May 2023 + description: + Welcome to Ethel + Morgan, who joined the MSP group as a Research Software + Engineer. + +- date: 14 April 2023 + description: + Thorsten Altenkirch visiting. + +- date: 1 April 2023 + description: + Welcome to Guillaume + Allais, who joined the MSP group as a Chancellor's Fellow. + +- date: 29 March 2023 + description: + Prakash Panangaden visiting. + +- start: 6 March 2023 + end: 14 March 2023 + description: + Nathaniel Virgo 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: + Jacques Carette visiting. + +- start: 18 July 2022 + end: 22 July 2022 + description: + We are organising the 5th international conference on + Applied Category + Theory. + +- date: 10 January 2022 + description: + Welcome to William + Waites, 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 CALCO 2021, + for his paper Tensor of Quantitative Equational Theories + with G. Bacci, P. Panangaden and G. Plotkin. + +- date: 1 August 2021 + description: + Jade + Master 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, Eigil + Rischel and Matteo + Capucci, 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 here. + +- date: 1 September 2020 + description: + Glynn Winskel and + Jules Hedges have joined the MSP + group. Welcome! + +- date: 2 March 2020 + description: + Welcome to Craig Roy who has joined MSP as a KTP Associate at Cambridge Quantum Computing. + +- 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 Bruno Gavranović, who + have joined the MSP group as a postdoc and a PhD student, + respectively. + +- date: 1 September 2019 + description: + Radu + Mardare is joining the MSP group. Welcome Radu! + +- start: 5 August 2019 + end: 9 August 2019 + description: + We are organising the first ever + Scottish Programming Languages and Verification Summer School. + +- 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: + Dan Ghica visiting. + + +- date: 10 May 2019 + description: + Troels Henriksen visiting. + +- start: 26 March 2019 + end: 1 April 2019 + description: + Johannes Marti visiting. + +- date: 11 March 2019 + description: + Welcome back Guillaume + Allais who is starting a postdoc with Conor McBride and Neil + Ghani. + +- start: 17 December 2018 + end: 18 December 2018 + description: + We are organising SYCO 2, the Second Symposium on Compositional Structures. + +- date: 14 December 2018 + description: + Robin Cockett 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 Scottish Programming Languages Seminar. + + +- date: 1 October 2018 + description: + Welcome to Malin Altenmüller who is starting a PhD in the MSP + group. + + +- start: 27 August 2018 + end: 31 August 2018 + description: + Philippa Cowderoy visiting. + + +- date: 9 August 2018 + description: + Ron Garcia visiting. + + +- start: 16 July 2018 + end: 20 July 2018 + description: + Jurriaan Rot visiting. + + +- date: 28 May 2018 + description: + Artem Shinkarov + visiting. + + +- start: 14 May 2018 + end: 30 May 2018 + description: + Helle Hvid Hansen + visiting. + + + +- start: 27 March 2018 + end: 28 March 2018 + description: + Thorsten Altenkirch visiting. + + +- date: 21 March 2018 + description: + Jamie Gabbay visiting. + + +- date: 7 February 2018 + description: + Justin Hsu visiting. + + +- start: 22 January 2018 + end: 26 January 2018 + description: + Jurriaan Rot visiting. + +- date: 6 December 2017 + description: + Chung-Kil Hur visiting. + + +- start: 23 October 2017 + end: 27 October 2017 + description: + Johannes Marti visiting. + + +- date: 11 September 2017 + description: + Andrea Vezzosi visiting. + + +- date: 27 July 2017 + description: + Matteo Cavaliere visiting. + + +- start: 10 July 2017 + end: 11 July 2017 + description: + We are organising a Workshop on Open Games. + + +- date: 5 July 2017 + description: + Noam Zeilberger visiting. + + +- date: 30 June 2017 + description: + Danel Ahman 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 Algebra and Coalgebra meet Proof Theory. + + +- date: 6 February 2017 + description: + Ohad + Kammar visiting. + +- date: 30 November 2016 + description: + We are organising the second meeting Categories, Logic, and Physics, Scotland. + + +- start: 21 November 2016 + end: 25 November 2016 + description: + Yde Venema + and Helle Hvid Hansen + visiting. + + +- date: 9 November 2016 + description: + We are organising a meeting of the Scottish Programming Languages Seminar. + + +- 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: + Jules Hedges visiting. + + +- date: 12 September 2016 + description: + "Congratulations to Federico Orsanigo for successfully defending his thesis "Bifibrational parametricity: from zero to two dimensions"!" + +- start: 12 September 2016 + end: 13 September 2016 + description: + Alex Simpson 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 Agda Implementors’ Meeting at Strathclyde. + + +- start: 29 February 2016 + end: 2 March 2016 + description: + Stephan Spahn visiting. + + +- date: 26 January 2016 + description: + Aleks Kissinger visiting. + + +- start: 25 January 2016 + end: 29 January 2016 + description: + John Power visiting. + +- date: 18 November 2015 + description: + Bram Westerbaan visiting. + + +- start: 19 October 2015 + end: 23 October 2015 + description: + Viktor Winschel visiting. + + +- start: 5 October 2015 + end: 9 October 2015 + description: + Alessandra Palmigiano 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: + Pierre Lescanne visiting. + + +- start: 14 September 2015 + end: 18 September 2015 + description: + Giovanni Cina visiting. + + +- start: 25 August 2015 + end: 29 August 2015 + description: + Julian Hedges visiting. + + +- date: 13 August 2015 + description: + Jeremy Siek visiting. + +- start: 25 May 2015 + end: 27 May 2015 + description: + Paul Levy visiting. + + +- date: 20 March 2015 + description: + Chris Heunen visiting. + +- date: 4 March 2015 + description: + We are organising A HoTT-Date with Thorsten Altenkirch — an afternoon of talks. + + +- start: 2 March 2015 + end: 6 March 2015 + description: + Thorsten Altenkirch visiting. + +- start: 20 January 2015 + end: 23 January 2015 + description: + James Chapman visiting. + +- start: 9 December 2014 + end: 10 December 2014 + description: + Aleks Kissinger visiting. + + + +- start: 26 September 2014 + end: 3 October 2014 + description: + Helle Hvid Hansen 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: + "Upcoming event: Workshop on Fibrations in Computer Science organised at Strathclyde." + + +- start: 4 June 2014 + end: 6 June 2014 + description: + The SICSA theme event + Practical Types + is organised by Neil and others, and attended by many of the MSP group. + + + + +- start: 28 May 2014 + end: 29 May 2014 + description: + Ohad Kammar visiting. + + +- date: 22 May 2014 + description: + Homotopy Type Theory reading group session on Higher Inductive Types will meet at Strathclyde. + + +- date: 15 April 2014 + description: +

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.

+ + +- date: 9 April 2014 + description: +

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

+ + +- date: 7 April 2014 + description: + Jamie Gabbay visiting. + +- start: 31 March 2014 + end: 4 April 2014 + description: + Thorsten Altenkirch visiting. + +- date: 16 August 2013 + description: + 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: + 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. + +- date: 4 August 2013 + description: + 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: + + 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 + + +- date: 23 July 2013 + description: + Alwin Blok will be joining the MSP group + to study for a PhD under Clemens expert supervision. + + +- date: 23 May 2013 + description: + 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: + Patricia Johann is organising this year's Parametricity Workshop at Strathclyde. + +- date: 1 January 2013 + description: + Clemens + Kupke has taken up a lectureship position within the + group. + +- date: 3 October 2012 + description: + 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: + 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. + + +- date: 15 June 2012 + description: + "Upcoming event: International Workshop on 75 Years of the λ-Calculus" + + +- date: 1 June 2012 + description: + 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. + + +- date: 25 May 2012 + description: + "Upcoming event: 6th Scottish Category Theory Seminar." + +- date: 2 May 2012 + description: + "Event Parametricity Workshop." + + +- date: 7 March 2012 + description: + "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.

" + + +- date: 10 February 2012 + description: + Scottish Theorem Provers Meeting + +- date: 19 December 2011 + description: + Peter Hancock at 60 + +

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

+ More information. + + +- date: 25 November 2011 + description: + 5th Scottish Category Theory Seminar + + +- date: 16 August 2011 + description: + 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/
+ + +- date: 4 August 2011 + description: + "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.

" + + +- start: 1 June 2011 + end: 2 June 2011 + description: + Bart Jacobs visited. + + +- date: 17 May 2011 + description: + "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." + + +- date: 13 May 2011 + description: + 4th Scottish Category Theory Seminar + + +- start: 21 April 2011 + end: 25 April 2011 + description: + Janis Voigtländer visited. + + +- date: 17 February 2011 + description: + 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. + +- date: 3 December 2010 + description: + "Algebraic Set Theory Course: Benno van den Berg" + + +- date: 2 December 2010 + description: + 3rd Scottish Category Theory Seminar + + +- start: 22 November 2010 + end: 26 November 2010 + description: + Wouter Swierstra visiting. + + +- date: 24 November 2010 + description: + Scottish Programming Languages Seminar diff --git a/_templates/default.html b/_templates/default.html index 86017b4..3354868 100644 --- a/_templates/default.html +++ b/_templates/default.html @@ -8,7 +8,7 @@ - {{Headtags}} + {{headtags}} diff --git a/css/pure.css b/css/pure.css new file mode 100644 index 0000000..0e548ae --- /dev/null +++ b/css/pure.css @@ -0,0 +1,34 @@ +:root { + --light-purple: #f1ebf9; +} + + +.recent-pubs h3.title { + border-bottom: none; + font-size: 100%; + margin-bottom: 1px; +} + +.recent-pubs p { + margin-top: 1px; +} + +.recent-pubs p.type { + font-size: 80%; +} + +/* We get some empty links from the RSS for some reason; make them not look like links */ +.recent-pubs a.link[href="#"] { + text-decoration: none; + cursor: default; +} + + +div.recent-pubs { + border-radius: 0.7em; + background: var(--light-purple); + padding: 1em; + padding-top: 0.1em; + margin-bottom: 1em; + min-width: 190px; +} diff --git a/news.html b/news.html deleted file mode 100644 index f61f7fc..0000000 --- a/news.html +++ /dev/null @@ -1,161 +0,0 @@ -### default.html(section.news=current) - -

News

- -

See also the MSP PURE page for a list of our recent papers, grants, etc.

- -
- -
5 May 2023
-
- Welcome to Iwan Quémerais, who is doing an internship with Clemens Kupke over the summer. -
- -
5 May 2023
-
- Johannes Marti visiting. -
- -
4 May 2023
-
- Welcome to Ethel Morgan, who joined the MSP group as a Research Software Engineer. -
- -
14 April 2023
-
- Thorsten Altenkirch visiting. -
- -
1 April 2023
-
- Welcome to Guillaume Allais, who joined the MSP group as a Chancellor's Fellow. -
- -
29 March 2023
-
- Prakash Panangaden visiting. -
- -
6 – 14 March 2023
-
- Nathaniel Virgo visiting. -
- -
8 November 2022
-
- Congratulations to Guillaume Allais for successfully passing his PhD viva with minor corrections! -
- -
September – December 2022
-
- Jacques Carette visiting. -
- -
18 – 22 July 2022
-
- We are organising the 5th international conference on Applied Category Theory. -
- -
10 January 2022
-
- Welcome to William Waites, who joined the MSP group as a Chancellor's Fellow. -
- -
1 October 2021
-
- Welcome to Dylan Braithwaite and Sean Watters, who are starting PhDs in the MSP group. -
- -
2 September 2021
-
- Congratulations to Radu who got the best paper award at CALCO 2021, for his paper Tensor of Quantitative Equational Theories with G. Bacci, P. Panangaden and G. Plotkin. -
- -
1 August 2021
-
- Jade Master has joined the MSP group. Welcome! -
- -
21 July 2021
-
- Welcome to Riu Rodríguez Sakamoto, who is starting a PhD in the MSP group. -
- -
1 July 2021
-
- Welcome to Ezra Schoen, who is starting a PhD in the MSP group. -
- -
1 October 2020
-
- Welcome to André Videla, Eigil Rischel and Matteo Capucci, who are starting PhDs in the MSP group. -
- -
25 September 2020
-
- Neil is giving weekly tutorial sessions on Open Games for MSP newcomers. Video recordings are available here. -
- -
1 September 2020
-
- Glynn Winskel and Jules Hedges have joined the MSP group. Welcome! -
- -
2 March 2020
-
- Welcome to Craig Roy who has joined MSP as a KTP Associate at Cambridge Quantum Computing. -
- -
6 January 2020
-
- Welcome to Georgi Nakov who is starting a PhD under the supervision of Fredrik Nordvall Forsberg. -
- -
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. -
- -
- -

Older News

- -

See here for older news.

diff --git a/old-news.html b/old-news.html deleted file mode 100644 index 2e3295e..0000000 --- a/old-news.html +++ /dev/null @@ -1,762 +0,0 @@ -### default.html(section.news=current) - -

Older News

- -

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

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