-
Notifications
You must be signed in to change notification settings - Fork 8
Expand file tree
/
Copy path101.yaml
More file actions
7055 lines (6826 loc) · 397 KB
/
101.yaml
File metadata and controls
7055 lines (6826 loc) · 397 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
usual:
usualTime: "13:00"
usualDay: "Monday"
usualRoom: "LT1414a"
usualBuilding: "Livingstone Tower"
talks:
- tag: Talk
date: '2026-02-12T16:00:00Z'
speaker: Shriram Krishnamurthi
speakerurl: https://cs.brown.edu/~sk/
institute: Brown University
insturl: https://cs.brown.edu
title: "Resugaring: Lifting Semantic Features through Syntactic Sugar"
abstract: |
Syntactic sugar is pervasive in language technology. It is used to shrink the size of a core language; to define domain-specific languages; and even to let programmers extend their language. Unfortunately, syntactic sugar is eliminated by transformation, so when the system provides feedback, it is in terms of a program that is unfamiliar to the authors. Thus, tool authors are forced to choose between their convenience and that of the programmer.
We address this conflict by showing how to lift core language features to present them in terms of the surface syntax. We have performed this research over three different features: execution traces, binding, and type rules. In each case we identify properties expected of the lifting and prove that our techniques satisfy these.
More broadly, though syntactic sugar is a central area of programming languages, it remains under-represented in the research literature. We briefly examine some other elements of a research agenda for this area.
location: LT1414a
material: []
- tag: Talk
date: '2026-03-30T13:00:00Z'
speaker: Sam Fish
speakerurl: ''
institute: MSP
insturl: ''
title: Categorical Quantum Nonlocality
abstract: |
After decades of being embroiled in political skirmishes, quantum physicists find themselves presented with a mathematical framework which predicts behaviour contrary to our reasonable intuitive leaning towards locality. Despite powerful attempts to quell the movement ensuing upon this realisation and to force it into irrelevance - even in the face of an incredibly successful experimental verification which no campaign can possibly diminish or sugar-coat - researchers now see no option but to accept the findings and to seek to understand their far reaches, along with anything they might reveal about quantum theory's relationship with relativity via Einstein's requirement of local causality.
On Monday I intend to present this timeline of escalation as faithfully as I can, along with some investigative findings, and some underlying categorical actors.
location: LT711
material: []
- tag: Talk
date: '2026-03-23T13:00:00Z'
speaker: Emma Tye
speakerurl: ''
institute: MSP
insturl: ''
title: (A very belated) Advert for POPL'26
abstract: |
So POPL'26 was 2 months ago. I went as a student volunteer, with my attendance funded by SIGPLAN and my travel funded by MSP. But what do I actually remember from it? What stood out? Did I see anything I think my fellow PhDs and professors would like?
I plan to give an overview of my first experience at a major conference as a student, as well as a whirlwind tour of some papers that caught my interest, or I think might catch yours!
location: LT711
material: []
- tag: Talk
date: '2026-03-16T13:00:00Z'
speaker: Clemens Kupke
speakerurl: ''
institute: MSP
insturl: ''
title: Thin behaviours, (co)algebraically (Part I)
abstract: |
In this talk I'll provide an update on our project on thin structures. Thin trees as introduced by Bojanczyk, Idziaszek and Skrzypczak are infinite trees with at most countably many infinite paths. While the theory of (top-down) automata operating on infinite trees is considerably less well-behaved than the one of automata on infinite words, thin trees provide a convenient setting where one can study tree-shaped data that behaves in some ways like words. In this talk I will recall the notion of a thin tree. I will then explain how thin trees generalise to the level of coalgebras for an analytic functor and how those thin "behaviours" can be seen as the quotient of an initial algebra of representants (terms of finite depth, but involving an infinitary operation). We axiomatize that quotient with a single equation. Underlying our result is a normal form theorem for thin behaviours. I will then sketch how thin behaviours might be useful in verification and/or model learning. The details of the latter will, however, most likely be the content for another 101.
This is joint work with Anton Chernev, Corina Cirstea and Helle Hvid Hansen.
location: LT711
material: []
- tag: CancelledTalk
date: '2026-03-09T13:00:00Z'
speaker: Fiona Blackett
speakerurl: ''
institute: MSP
insturl: ''
title: TBC
abstract: ''
location: LT711
material: []
- tag: Talk
date: '2026-03-02T13:00:00Z'
speaker: Vikraman Choudhury
speakerurl: ''
institute: MSP
insturl: ''
title: Inceptions
abstract: |
We can program with continuations using the continuation monad, which gives us control operators, control effects, and classical logic. But, it is not an algebraic effect, and corresponds to a large algebraic theory. Is there a monad for non-local control effects, which is still algebraic?
This is work-in-progress, and based on joint work with Gregor Feierabend and Marcelo Fiore.
location: LT711
material: []
- tag: Talk
date: '2026-02-23T13:00:00Z'
speaker: Fredrik Nordvall Forsberg
speakerurl: ''
institute: MSP
insturl: ''
title: Introduction to setoids
abstract: |
A setoid is a type X together with an equivalence relation ≅_X : X → X → Prop, i.e. ≅_X is reflexive, symmetric, and transitive. Setoids are widely used in (pre-HoTT) type theory based approaches to constructive mathematics, where quotients might not be available, or better avoided for computational reasons. Even though setoids have a bad reputation ("setoid hell") due to a quickly leading to a lot of boilerplate, I'll argue that they are quite nice to work with as a model construction, as setoids validate many convenient axioms such as function extensionality and countable choice.
location: LT711
material: []
- tag: Talk
date: '2026-02-16T13:00:00Z'
speaker: Conor McBride
speakerurl: ''
institute: MSP
insturl: ''
title: Finitary testing
abstract: ''
location: LT307
material: []
- tag: Talk
date: '2026-02-09T13:00:00Z'
speaker: Rin Liu
speakerurl: ''
institute: MSP
insturl: ''
title: Structural Set Theory
abstract: |
Suppose you were asked, "is 3 ∈ ℕ?" Being a natural number, 3 is indeed a member of ℕ, so the answer is “yes”. On the other hand, the question, “is π ∈ ℚ?”, would quickly receive an answer of “no”. Now, suppose you were then asked, “is π ∈ log?”
You’d might pause for a moment, before again answering in the negative, but for a different reason than before. After all, π is a number, and log is a function, so π being a member of log -- whatever that means -- would be ridiculous! A better answer might be to declare the question as meaningless.
As computer scientists and/or type theorists, the problem here is obvious. But in the foundations used in most mathematics outside of (higher) category theory, the issue is less clear-cut. In most common presentations of set-theoretic foundations -- for our purposes, ZFC; Zermelo–Fraenkel set theory with Choice -- everything is a set, so the question “is π ∈ log?” should have a yes-or-no answer.
Many of these kinds of quirks arise from the "global" nature of the set membership relation: it is always valid to compare any two arbitrary sets for membership and equality. However, in most practical contexts, sets are often stratified, in the sense that we usually don’t have very long chains of membership containment, and sets from different strata are very rarely compared or combined. This talk aims to present the structuralist's approach to this problem: a categorical way of constructing "structural" sets connected together via only local set membership relations between them that avoids these kinds of problems. This talk is intended to be accessible and expository, and requires only basic exposure to category theory.
location: LT209
material: []
- tag: Talk
date: '2026-02-02T13:00:00Z'
speaker: Guillaume Allais
speakerurl: ''
institute: MSP
insturl: ''
title: Trees for Concurrency
abstract: |
Looking at Claessen's 1999 functional pearl "A poor man's concurrency monad", we will see how we can simulate a limited form of concurrency in purely functional terms. We will then go on to see how to modify the setup to return a value from that computation as well as introduce join points.
location: LT209
material: []
- tag: Talk
date: '2026-01-26T13:00:00Z'
speaker: Ezra Schoen
speakerurl: ''
institute: MSP
insturl: ''
title: Species of Trees
abstract: |
Mathematicians and computer scientists both enjoy trees very much. I know I certainly do, and I wish to share my enthusiasm. This talk will be a theory-light tour of various interesting phenomena relating to species of trees. We will discuss what makes a species, what makes a tree, and look at a range of particularly interesting examples of species of trees. In the interest of managing expectations: you're not likely to learn all that much about combinatorial species from this talk. It's more of an excuse to have a fun and relaxed time exploring ways trees can occur 'in the wild'.
location: LT209
material: []
- tag: Talk
date: '2026-01-19T13:00:00Z'
speaker: Conor McBride
speakerurl: ''
institute: MSP
insturl: ''
title: Wiggle It (Just a Little Bit)
abstract: |
Testing can reveal the absence of bugs in situations where we can show that the test data expose all the possible variations. This is straightforward when the domain is finite, but one can also achieve test coverage for large domains by restricting the ways in which the program may process its input. For example, the fact that the sum of the numbers less than n is n choose 2 can be proven by testing for n in {0, 1, 2} because both calculations are inherently quadratic. I have, on and off, been thinking about how to deliver similar results for other inductive data structures. For example, one can generate particularly well behaved folds on unlabelled binary trees by giving (i) the tree which is the image of the leaf, and (ii) a tree with two variables showing how the ouptut for a node is computed from the outputs for its two subtrees. I claim that if two such folds agree at the four smallest trees, then they agree for all trees. Clearly, we recover (i) by testing at a leaf. We recover (ii) by testing at a node with leaves for subtrees, then perturbing each of those subtrees in turn, to see where the output changes. That is to say, we use perturbation to recover abstraction. I am currently working on a proof of this claim in Agda and will share my progress (and my prospectus) in this talk.
location: LT210
material: []
- tag: Talk
date: '2025-12-15T13:00:00Z'
speaker: Ezra Schoen
speakerurl: ''
institute: MSP
insturl: ''
title: Duality
abstract: ''
location: TBD
material: []
- tag: Talk
date: '2025-12-11T15:00:00Z'
speaker: Noam Zeilberger
speakerurl: 'https://noamz.org/'
institute: Laboratoire d'informatique de l'École Polytechnique
insturl: ''
title: The free bifibration on a functor
abstract: |
Joint work with Bryce Clarke and Gabriel Scherer.
Preprint: https://arxiv.org/abs/2511.07314
A functor p : D → C is a bifibration if, loosely speaking, one can push and pull objects of D along arrows of C. The talk will begin by recalling the formal definition together with some motivation, and then explain how the free bifibration generated by a functor p may be constructed using a simple sequent calculus. This sequent calculus is closely related to a certain "zigzag double category" ℤC constructed as the free bifibration on the identity functor id : C → C, and which is also the free fibrant double category on C. The double category perspective leads to a nice string diagram calculus, while proof-theoretic techniques allow us to derive a canonicity result for free bifibrations, and to analyze some examples of a combinatorial nature.
location: LT310 and online
material: []
- tag: CancelledTalk
date: '2025-12-08T13:00:00Z'
speaker: Guillaume Allais
speakerurl: ''
institute: MSP
insturl: ''
title: TBD
abstract: ''
location: TBD
material: []
- tag: Talk
date: '2025-12-09T14:00:00Z'
speaker: Jan de Muijnck-Hughes
speakerurl: ''
institute: MSP/StrathCyber
insturl: ''
title: An Introduction to Design-by-Contract with Dafny
abstract: |
Dafny is a multi-paradigm language with deep integration of <strong>design-by-contract</strong> style verification: Hoare Triples. What makes Dafny interesting from a language design perspective is that, although, there is a clear separation between a specification and the code it reasons about, specifications are nonetheless made from code. For this 101, I am going to introduce everyone to Dafny and show how one can write and reason about simple imperative and object-oriented programs and their behaviour.
What excites me about Dafny is its potential to act as a <em>bridging language</em> that guides students, who are ostensibly rooted in imperative programming, through to the world of verification without having to introduce them to the world of dependently-typed functional programming. I hope you will be excited about Dafny too.
location: LT1414a
material: []
- tag: Talk
date: '2025-11-24T13:00:00Z'
speaker: Vikraman Choudhury
speakerurl: ''
institute: MSP
insturl: ''
title: Semantic analysis of Polarization
abstract: Polarization is a proof-theoretic technique used to study various kinds of logics with classical dualities. I will give a model-theoretic explanation of polarization in the context of classical logic and classical linear logic (Girard and Laurent). Finally, I will show a higher-dimensional generalisation of these ideas to generalised species.
location: LT310 and online
material: []
- tag: Talk
date: '2025-11-17T13:00:00Z'
speaker: Clemens Kupke
speakerurl: ''
institute: MSP
insturl: ''
title: Graph Games with Infinite Plays
abstract: In this 101 I am planning to discuss 2-player graph games with infinite plays. At first we will focus on games with "trivial" acceptance conditions where a player either loses or wins all infinite plays. As motivating example I will present the games that characterize least and greatest fixpoints of monotone operators. After that we will explore why those games are too simple for reasoning about alternating fixpoints and move to parity games, a type of graph game that captures the full expressive power of the modal mu calculus. Time permitting I will explain how to prove that parity games are (memoryless) determined and how one can compute winning regions of a given parity game.
location: LT1414a and Online
material: []
- tag: Talk
date: '2025-11-10T13:00:00Z'
speaker: Ohad Kammar
speakerurl: https://denotational.co.uk/
institute: University of Edinburgh
insturl: ''
title: Modular abstract syntax trees (MAST) – substitution tensors with second-class sorts
abstract: |
We adapt Fiore, Plotkin, and Turi's treatment of abstract syntax with binding, substitution, and holes to account for languages with second-class sorts. These situations include programming calculi such as the Call-by-Value λ-calculus (CBV) and Levy's Call-by-Push-Value (CBPV). Prohibiting second-class sorts from appearing in variable contexts means the presheaf of variables is no longer a left-unit for Fiore et al's substitution tensor product. We generalised their development to associative and right-unital skew monoidal categories. We reuse much of the development through skew bicategorical arguments. In ongoing work, we replace the skew monoidal structure with ordinary monoidal structure by recourse to substitution modules instead of substitution monoids.
We apply the resulting theory in two scenarios. We employ the mathematical theory to circumvent the expression problem when proving substitution lemmata for varieties of CBV denotational semantics modularly. We employ a computational implementation of the theory to circumvent the expression problem when implementing intrinsically-typed foreign-function interfaces for the 29 theories of SMTLIB.
Joint work with Marcelo Fiore, Kajetan Granops, Mihail-Codrin Iftode, Georg Moser, and Sam Staton.
location: LT1414a and Online
material: []
- tag: Talk
date: '2025-11-04T16:00:00Z'
speaker: Georgi Nakov
speakerurl: ''
institute: MSP
insturl: ''
title: Matrix Type Theory
abstract: |
What is an appropriate type for a matrix, and what are the accompanying typing rules? Depending on your mileage, the answer might seem obvious or dull — can't we start with a humble <tt>Matrix A m n</tt>? I would argue that better candidates exist, and that suitable typing rules are far from obvious, at least if we aim at actually implementing the said rules. In this talk, I will embark on the long journey of turning something that looks good on paper into something that works in code. We try to abolish any implicit assumptions, hidden computation and blind guessing from the initial typing rules, and refine them until they can guide a precise implementation. With guest occurrences of the usual suspects — bidirectional typing, thinnings, and typecheckers-that-get-to-know-monoid-laws.
location: LT1414a and Online
material: []
- tag: Talk
date: '2025-10-27T13:00:00Z'
speaker: Sean Watters
speakerurl: ''
institute: MSP
insturl: ''
title: What I did in my PhD
abstract:
The modal μ-calculus is a modal logic that type theorists don't usually spare much thought for; it's usually treated classically, and its main application is as a specification language for model checking, where it subsumes weaker but more commonly used logics like LTL, CTL, and PDL. Meanwhile, modal logicians study the μ-calculus using very "1930s" concepts like explicitly named variables. Most of my efforts during my PhD have been spent trying to pull the theory of the modal μ-calculus into this century (AKA into Agda) using the tools of type theory, but my real interest is in what we type theorists might glean from the exchange. For example, the modal μ-calculus is a fixpoint logic, with a very mature account of fixpoint alternation - something that every proof assistant (to my knowledge) is lacking.
In this talk, I'll be using the μ-calculus and some of my recent work on it as a motivating example to give a slightly non-standard introduction to some important MSP ideas - syntaxes with binding, and data types as fixpoints. I'll cover the least fixpoint (which computer scientists love), the greatest fixpoint (which we sometimes tolerate), and the rational fixpoint (which many forget exists, but plays a key role in my work). If time permits, I'd also like to open the door to the terrifying world of arbitrary fixpoint alternation, and some (very very early) ideas for taming it.
location: LT310 and Online
material: []
- tag: Talk
date: '2025-10-20T13:00:00Z'
speaker: Bob Atkey
speakerurl: ''
institute: MSP
insturl: ''
title: Capucci Logic
abstract: |
For some applications, it is useful for the truth of a logical statement to be approximate instead of merely true or false. Fuzzy Logics are a famous example of such logics, where statements are valued in the interval [0,1], where 1 represents "definitely true" and 0 represents "definitely false".
In this talk, I'll talk about a logic which is valued in [0,∞] where implication is interpreted as a ratio between premises and conclusion. The main feature of this logic is that we can formulate a logic where the "sharp" lattice connectives are replaced by smooth ones. Our hope is that this will allow such logics to be used in situations where satisfiability can be learned, or where non-satisfaction is treated as a cost during training.
location: LT310 and online
material: []
- tag: Talk
date: '2025-10-13T13:00:00Z'
speaker: Fiona Blackett
speakerurl: ''
institute: MSP
insturl: ''
title: Introduction to Persistent Homology
abstract: ''
location: LT1414a and Online
material: []
- tag: Talk
date: '2025-10-10T16:00:00Z'
speaker: Fredrik Nordvall Forsberg
speakerurl: ''
institute: MSP
insturl: ''
title: An introduction to constructive logic
abstract: Constructive logic (also known as intuitionistic logic) is logic without
the Law of the Excluded Middle, which states that P or ¬ P holds for every proposition
P. Hilbert famously said that denying mathematicians the use of the Law of the
Excluded Middle is "the same as denying the boxer the use of his fists". I will
try to convince you that there sometimes is merit in not trying to punch people
in the head. For example, constructive logic is the internal logic of toposes,
and so a constructive proof can often be reinterpreted to show a much stronger
result than a classical one, e.g., a constructed proof of the existence of a function
might in fact automatically yield the existence of a <em>continuous</em> or <em>computable</em>
function. Constructive logic often leads to interesting mathematics, as it allows
for finer distinctions than classical logic. I will also discuss how and when,
despite appearances, constructive logic can be seen as an extension of classical
logic, rather than as a restriction.
location: LT210 and online
material: []
- tag: Talk
date: '2025-10-03T16:00:00Z'
speaker: Jeremy Singer
speakerurl: https://www.dcs.gla.ac.uk/~jsinger/
institute: University of Glasgow
insturl: https://www.gla.ac.uk/schools/computing/
title: Let's Take Esoteric Programming Languages Seriously
abstract: Esoteric programming languages are challenging to learn, but their unusual
features and constraints may serve to improve programming ability. From languages
designed to be intentionally obtuse (e.g. INTERCAL) to others targeting artistic
expression (e.g. Piet) or exploring the nature of computation (e.g. Fractan),
there is rich variety in the realm of esoteric programming languages. This essay
examines the counterintuitive appeal of esoteric languages and seeks to analyse
reasons for this popularity. We will explore why people are attracted to esoteric
languages in terms of (a) program comprehension and construction, as well as (b)
language design and implementation. Our assertion is that esoteric languages can
improve general PL awareness, at the same time as enabling the esoteric programmer
to impress their peers with obscure knowledge. We will also consider pedagogic
principles and the use of AI, in relation to esoteric languages. Emerging from
the specific discussion, we identify a general set of "good" reasons for designing
new programming languages. It may not be possible to be exhaustive on this topic,
and it is certain we have not achieved that goal here. However we believe our
most important contribution is to draw attention to the varied and often implicit
motivations involved in programming language design.
location: LT1414a and Online
material: []
- tag: Talk
date: '2025-09-22T13:00:00Z'
speaker: Conor Mc Bride
speakerurl: ''
institute: MSP
insturl: ''
title: 'Leftovers, Rightunders: Typechecking Thinnings Compositionally'
abstract: |-
In the interests of sharing MSP lore, I came up with a way to talk about both the "Input Subject Output" approach to typechecking and the Category of Thinnings in the same talk, making the latter an interesting example of the former.
The Input Subject Output approach, like most bidirectional approaches to problem decomposition, tracks whether signals go from parent to child or vice versa, but it also acknowledges a signal has a guarantor as well as a sender, responsible for the meaningfulness of the signal. Meanwhile, thinnings are order-preserving embeddings between ordered sequences, or dually, selections of elements from sequences (their resemblance to binomial coffecients is no accident), and are thus a fine example of a monoidal category.
I won't assume that any of you know know any of this: many of us do; more of us should. And I'll try to tell the story with pictures, drawn on a whiteboard, rather than jargon.
I often use thinnings to talk about embeddings between scopes, the latter seen as sequences which grow on the right (because of prejudices about time). A compositional way to typecheck a thinning is to start with the available stuff "over" the thinning, together with a thinning that will start choosing from the newest stuff on the right. If all is well, we shall learn which "leftovers" have not yet been considered, and which "rightunders" have been not only considered but also selected. There is a healthy story about both the monoidal/parallel/spatial/tensor structure of thinnings and their categorical/sequential/temporal/composition structure, yielding an algorithm which never has to guess where to chop sequences in two.
location: LT1310 and Online
material:
- tag: Link
address: https://www.youtube.com/watch?v=BABpO4epxOo
linkDescription: Video
- tag: SpecialEvent
date: '2025-09-18T16:05:00Z'
endDate: '2025-09-18T17:00:00Z'
title: MSP101 Planning meeting
url: ''
location: LT1414a and Online
locationurl: ''
description: ''
- tag: Talk
date: '2025-05-30T14:00:00Z'
speaker: Liang-Ting Chen
speakerurl: https://l-tchen.github.io/
institute: Institute of Information Science, Academia Sinica, Taiwan
insturl: https://www.iis.sinica.edu.tw/en/index.html
title: A formal treatment of bidirectional typing
abstract: 'In this talks, we consider a general and formal theory of bidirectional
typing for simply typed languages: for every signature that specifies a mode-correct
bidirectionally typed language, there exists a proof-relevant type synthesiser
which, given an input abstract syntax tree, constructs a typing derivation if
any, gives its refutation if not, or reports that the input does not have enough
type annotations.<br>Sufficient conditions for deriving a type synthesiser such
as soundness, completeness, and mode-correctness are established for all signatures.
We propose a preprocessing step, which helps the user to deal with missing type
annotations. The entire theory is implemented in Agda, serving as a verified generator
of proof-relevant type synthesisers as a by-product.'
location: LT210 and Online
material: []
- tag: SpecialEvent
date: '2025-05-28T11:00:00Z'
endDate: '2025-05-28T12:00:00Z'
title: ADR/Promotion Information Meeting
url: ''
location: LT1414a
locationurl: ''
description: ''
- tag: Talk
date: '2025-03-19T16:00:00Z'
speaker: Petar Veličković
speakerurl: https://petar-v.com/
institute: Google DeepMind
insturl: https://deepmind.google/
title: Generalisation in LLMs
abstract: A general talk about our recent works on generalisation in llms
location: LT210 and Online
material:
- tag: Link
address: https://youtu.be/7Z144Ymohd0
linkDescription: Video
- tag: CancelledTalk
date: '2025-03-19T11:00:00Z'
speaker: Matthew Cartmell
speakerurl: https://www.strath.ac.uk/staff/cartmellmatthewprofessor/
institute: Department of Mechanical and Aerospace Engineering
insturl: ''
title: Symbolic Computational Dynamics
abstract: |-
The term 'symbolic computational dynamics' has evolved over time and has been promoted by ourselves over the years to describe our interdisciplinary research in engineering dynamics, applied mathematics, and symbolic computation and has now gained recognition and some acceptance in the nonlinear dynamics community. This research has been based on a combination of the modelling of time-variant mechanical systems (mostly) using classical equation derivation techniques such as Newton-Euler and Lagrange, the approximate analytical solution of the ODEs, PDEs / BCs, or DAEs that have been derived using appropriate asymptotic methods, and finally the symbolic computation needed to make this whole process as automated and scalable as possible.
Symbolic Computational Dynamics has its roots in the 1970s when early codes such as MACSYMA emerged, and then gained further traction in the later 1980s with the advent of codes such as Maple and Mathematica. It has evolved into a more structured research activity in recent years and this seminar will attempt to summarise some of the principal milestones along the way. The mathematical challenges posed by vibration theory have been exceptionally useful for developing practical algorithmic structures for various asymptotic mathematical methods for approximate solution, notably methods such as Lindstedt-Poincaré, Poincaré-Lighthill, Krylov-Bogoliubov, general averaging, and the method of multiple scales. These experiments with manual analysis started in the early 1980s and eventually led to the development of precursor codes in Mathematica. We started to adopt this code quite early on in our research due to its robustness and powerful functionality. This decision has affected our work significantly, in ways that have continued to work reasonably to our advantage, and we have developed several prototype solvers, mostly exploiting the powerful and adaptable method of multiple scales over the alternatives.
EPSRC funding was first awarded in 1997 and several grants followed, enabling a small research team to be sustained for the following fifteen years. The findings of that period enabled several specialised studies to follow and further PhDs focusing on solver refinements and some initial work on symbolic code for the semi-automated derivation of differential equation models for low dimensional systems.
In 2020 the start-up company Symbolic Computational Dynamics Ltd (SCD Ltd) was founded, and sufficient private investment was obtained for the co-funding of a further PhD. In 2024 SCD Ltd was proposed for possible spin-out conversion through the University of Strathclyde’s Stage Gate company development programme. This has led to highly significant business development support for a focused programme of product development, with the intention to enter a high growth phase so that SCD software products can be brought to the market within 12 to 15 months.
This seminar will outline some of the contributions that we have made to the field of symbolic computational dynamics, and the development of our software to the point where commercial products can be planned.
location: LT? and Online
material: []
- tag: CancelledTalk
date: '2025-04-28T15:00:00Z'
speaker: Justus Matthiesen
speakerurl: ''
institute: University of Edinburgh
insturl: ''
title: TBD
abstract: ''
location: LT412 and Online
material: []
- tag: Talk
date: '2025-04-22T15:00:00Z'
speaker: April Gonçalves
speakerurl: ''
institute: MSP
insturl: ''
title: A quick & dirty look at at abstract syntax with binders and metavariables
abstract: In this talk, I will show the (categorical) semantics of Fiore and collaborators’
“Second-Order Abstract Syntax with Binders” and of McBride and collaborators’
“Universe of Syntaxes with Bindings”. I will also compare them under multiple
criteria (literature, usage, meta theory and implementation/formalisation), with
special focus on how both approaches handle metavariables by using System F as
our main example. (Please beware it’s a work in progress, and many details haven’t
been worked out yet
location: LT210 and Online
material:
- tag: Link
address: https://youtu.be/kwSeO50FBFE
linkDescription: Video
- tag: Talk
date: '2025-04-07T15:00:00Z'
speaker: Aven Dauz
speakerurl: ''
institute: MSP
insturl: ''
title: Modelling cybersecurity games with compositional game theory
abstract: Compositional game theory and its corresponding Haskell DSL <q>open-games-engine</q>,
have been used for modelling microeconomic games, auctions, and smart contracts.
Some advantages of this compositional approach are leveraging modularity and code-reuse
to construct larger games. Incidentally, game theory has been used to model complex
attack-defense scenarios in cybersecurity, with the simplest case modelling the
strategic interaction between a single attacker and defender. Scaling these models
to accurately reflect real-world attacks and extrapolate data to improve the performance
of systems remains an active area of research. In this talk I'll present a honeypot
allocation game and design choices that allow a modeller to easily extend the
construction to represent defensive strategies such as deception.
location: LT412 and Online
material:
- tag: Link
address: https://youtu.be/JBOcJW_kxy8
linkDescription: Video
- tag: CancelledTalk
date: '2025-03-31T15:00:00Z'
speaker: Philippa Cowderoy
speakerurl: ''
institute: ''
insturl: ''
title: TBD
abstract: ''
location: LT412 and Online
material: []
- tag: Talk
date: '2025-03-17T15:00:00Z'
speaker: Ross Horne
speakerurl: ''
institute: MSP
insturl: ''
title: Additives without Weakening
abstract: As we know, in linear logic, conjunction and disjunction decompose into
separate multiplicative and additive forms. Only additives are idempotent in general
(A + A --o A). The additives also have some properties such as weakening (A &
B --o A). By dropping weakening, the additives further decompose into infinitely
many <q>sub-additive</q> operators. <p>I explain how I spotted these sub-additive
operators when studying nominal quantifiers that can similarly be decomposed into
new nominal quantifiers. I found these new additives curious since the resulting
operators have properties that are sound with respect to probability distributions,
effectively internalising probability distributions in logic. I end by giving
a taste of the proof theory of the sub-additives. A novelty is that, due to how
sub-additives control certain distributivity properties that play an essential
role in established cut elimination techniques, a new proof technique must be
invented.</p>
location: LT412 and Online
material:
- tag: Link
address: https://youtu.be/04K0vkcqXvU
linkDescription: Video
- tag: Talk
date: '2025-03-10T15:00:00Z'
speaker: Zanzi Mihejevs
speakerurl: ''
institute: GlAiVe Research
insturl: https://glaive-research.org/
title: A canonical bidirectional typing discipline through polarised System L
abstract: What is the relationship between polarity and bidirectional typing? It
has long been observed that there is a connection between the two, but the precise
relationship has remained unclear. Moreover, it has been argued that the link
itself is a red herring, and that bidirectional typing is better explained not
by polarity but by chirality - the duality between producers and consumers. <p>In
this talk we will look at Polarised System L, a type theory that combines both
dualities - the positive fragment is driven by a cut between a primitive producer
and a pattern, and the negative fragment is driven by a cut between a primitive
consumer and a co-pattern.</p> <p>Remarkably, linear System L admits a canonical
bidirectional typing discipline based on a combination of ideas from both standard
and co-contextual typing, giving us a <q>bi-contextual</q> typing algorithm.</p>
<p>We will see how this lets us equip a type system based on full classical linear
logic - containing all four connectives and derivable implication and co-implication
- with a bidirectional discipline where all typing annotations are exclusively
limited to shifts between sythesisable and checkable expressions.</p>
location: LT412 and Online
material:
- tag: Link
address: https://youtu.be/0Qg_RnSHyhU
linkDescription: Video
- tag: Talk
date: '2025-03-03T15:00:00Z'
speaker: Fredrik Nordvall Forsberg
speakerurl: ''
institute: MSP
insturl: ''
title: Representing type theory in type theory
abstract: It is often claimed that type theory can act as a foundation of mathematics.
If that is so, then type theory should in particular be able to reason about type
theory itself. Of course, Dr Gödel points out that this cannot work, in general,
but we would expect that type theory could still reason about a slightly weaker
version of itself. This turns out to be true, but messy, because type theory is
quite complicated as a theory. After heroic attempts by Danielsson (2006) and
Chapman (2009) to represent type theory internally in type theory, Altenkirch
and Kaposi (2016) made a breakthrough in using so-called quotient inductive-inductive
types to represent the well typed terms of type theory, where quotient constructors
are used to encode beta and eta laws as equalities in the type. Being able to
treat such laws as actual equalities is a major improvement, but quickly leads
into so-called <q>transport hell</q>, where explicit transports along equalities
show up in terms and needs to be reasoned about. I will report on some recent
work together with Liang-Ting Chen and Tzu-Chun Tsai on how one can use experimental
(and hopefully future) features of Agda to improve on the quotient inductive-inductive
representation and remove most uses of transport.
location: LT412 and Online
material: []
- tag: Talk
date: '2025-02-24T15:00:00Z'
speaker: Robert Atkey
speakerurl: ''
institute: MSP
insturl: ''
title: Semantic proofs of Cut-elimination for Deep Infererence
abstract: 'Deep Inference systems are a kind of proof calculus that allow inference
rules to be applied anywhere in a formula. Cut-elimination for these systems is
similar to that for Sequent calculi: rules that introduce intermediate formulas
can be removed from proofs. Prior proofs of cut-elimination relied on intricate
syntactic method. I''ll talk about a semantic approach that builds a model of
the whole calculus from cut-free proofs, such that every proof constructed in
this model can be read back as a cut-free proof. This is a similar technique to
the one used in Normalisation by Evaluation (NbE). The technique is very flexible
and extends to many extensions of Multiplicative Linear Logic, including BV''s
self-dual non-commutative <q>before</q> connective, additives, and exponentials.
<p>This is joint work with Wen Kokke and was published at MFPS last year: https://bentnib.org/sem-cut-elim-mfps.html</p>'
location: LT412 and Online
material:
- tag: Link
address: https://youtube.com/live/urIEmeRuxTU
linkDescription: Video
- tag: Talk
date: '2025-02-17T15:00:00Z'
speaker: Clovis Eberhart
speakerurl: ''
institute: MSP
insturl: ''
title: Weakest Precondition of Open Coalgebras
abstract: Coalgebras are a categorical framework that have proved useful to describe
and reason about different types of systems. We define open coalgebras, a compositional
framework where coalgebras can be composed as string diagrams. We give them a
semantics in terms of weakest precondition predicate transformers computed as
a fixed point and link it to previous work on weakest precondition predicate transformers
by Aguirre, Katsumara, and Kura. We give several examples of verification problems
this semantics can compute, showing its practical usefulness. We give conditions
under which this semantics is compositional for the string diagram structure of
open coalgebras. Finally, we give a syntactic precomputation of open coalgebras
that removes their internal states while preserving their semantics.
location: LT1414a and Online
material: []
- tag: Talk
date: '2025-02-10T15:00:00Z'
speaker: Ezra Schoen
speakerurl: ''
institute: MSP
insturl: ''
title: Coequations via proof systems
abstract: "<p><b>What even is a coequation?</b> While Universal Algebra enjoys a
set-in-stone consensus on both the correct syntax of equations, as well as what
an equation even is, Universal Coalgebra is in no such position. There are many
attempts at definitions and syntaxes of coequations, but it is hard to say which
one is 'the correct one'.</p> <p>Rather than sorting out this mess, why not add
yet another proposal? If we squint, we can see proof systems for modal logic as
coequations. This then leads to some fun, natural questions. Which coequations
can be captured by what kind of proof systems? If we restrict our attention to
a class of 'simple' systems, can we specify <q>every</q> coequation?</p> <p>As
this is work in progress, I have a fewer answers than questions. The aim of this
talk is to introduce coequations in all their colours, and to get the audience
to a point where the questions may be appreciated.</p>"
location: LT209 and Online
material:
- tag: Link
address: https://youtu.be/VCfCkAwK2pg
linkDescription: Video
- tag: Talk
date: '2025-02-03T15:00:00Z'
speaker: Jules Hedges
speakerurl: ''
institute: MSP
insturl: ''
title: We solved dependent optics!
abstract: "<p>There are two major generalisations of lenses. First there are optics,
which require almost nothing of their base category and give you something in
return. And then there are dependent lenses (aka container morphisms, aka natural
transformations of polynomials), which require a lot of their base category but
give you even more in return. One day several years ago I innocently twote the
question of how to unify these two constructions, which is motivated for mathematical,
computational and sociological reasons. The problem ended up occupying us (joint
work with Dylan Braithwaite, Matteo Capucci, Bruno Gavranović, Eigil Rischel and
André Videla) for several years, and its difficulty became a meme.</p> <p>I will
explain the answer that finally satisfied us. This involves first constructing
a category of <q>dependent adaptors</q> and then freely adjoining a particular
family of monoidal costates using a technique we call <q>weighted coparametrisation</q>
that we reinvented. The definition began life as a prototype in Idris using QTT
features, and was then translated back into category theory using what might or
might not be a novel semantics of polymorphic dependent type theory.</p>"
location: LT209 and Online
material:
- tag: Link
address: https://youtu.be/yhxwUnWKK2I
linkDescription: Video
- tag: Talk
date: '2025-01-27T15:00:00Z'
speaker: André Videla
speakerurl: ''
institute: MSP
insturl: ''
title: Pipelining and dependent types
abstract: Pipelining is a crude CPU optimisation to speed up execution of sequential
programs. By allowing the manipulation of types as values, dependent types enable
new abstractions to manipulate large-scale of software based on sequential computation
inspired by CPU pipelining. I will show how to define pipelines, sequential programs
that cannot easily be parallelised using a list of types as a specification. Given
this list of type, the implementation of a pipeline is given by the functions
between each type. This pipeline abstraction can be generalised to categories
such that the pipeline is made up of objects and its implementation is given by
the morphisms between them. This enable the use of kleisli morphisms for effectful
programs. The pipeline can be further abstracted over graded categories enabling
automatic composition of errors. Finally, I will show how to use dependent pipelines
to allow composition of programs with type-dependency. An architecture particularly
useful for single-pass compilers with well-scoped and well-typed implementations.
location: LT412 and Online
material:
- tag: Link
address: https://youtu.be/dQU4IA1hDa4
linkDescription: Video
- tag: Link
address: https://gitlab.com/avidela/types-laboratory/-/blob/main/src/MSP101Cheat.idr?ref_type=heads
linkDescription: Code of the talk
- tag: Link
address: https://gitlab.com/glaive-research/pipelines
linkDescription: Library code
- tag: Talk
date: '2025-01-20T15:00:00Z'
speaker: Conor McBride
speakerurl: ''
institute: MSP
insturl: ''
title: My Favourite Double Category
abstract: I'll (re)introduce the <q>codeBruijn</q> representation of syntax with
binding, in which terms are intrinsically indexed over their support (the variables
they are involved with) rather than their scope. These supports form the objects
of a category of order-preserving injections (<q>thinnings</q> to MSP locals and
<q>my triangle</q> to Blaise Pascal), whose dual (<q>selections</q>) plays a crucial
role in managing the restrictions of the variable support in specific substructures.
Meanwhile, the notion of <q>simultaneous substitution</q> tightens to a relevant
structure where every variable in the source support has an image, and every variable
in the target support is used by at least one of those images. The action of substitution
(which includes substitution composition) respects support precisely. It is reliant
on the way a selection from a substitution's source support variables retains
only some of their images and is itself relevant only once we have identified
the corresponding selection from the target support of only those variables used
in the retained images. We acquire squares with selections for vertical edges
and relevant substitutions for horizontal edges which compose in both dimensions,
forming a double category. (For anyone who saw, or for that matter, gave Phil
Wadler's talk at the last SPLS, codeBruijn shifting happens at the root of a term,
obviating the complex relationship between renaming and substitution which happens
only because de Bruijn shifting happens at the leaves.) (For dependently typed
programmers, more generally, there may be transferable lessons in managing coherence.)
location: LT412 and Online
material:
- tag: Link
address: https://youtu.be/aAgqu1y4Xto
linkDescription: Video
- tag: SpecialEvent
date: '2025-01-17T13:30:00Z'
endDate: '2025-01-17T14:30:00Z'
title: MSP101 Planning meeting
url: ''
location: LT1414a and Online
locationurl: ''
description: ''
- tag: Talk
date: '2025-01-17T13:00:00Z'
speaker: April Gonçalves
speakerurl: ''
institute: MSP
insturl: ''
title: Type-Sensitive Algebraic Macros
abstract: Despite recent advances made by Idris and Lean teams, metaprogramming
in a typed language is still hard, frustrating and error-prone. In this short
paper, we investigate a new view on macros via a type-sensitive algebraic theory
for typechecker scripting for a more principled approach to type-directed macros.
We show that our theory encodes typechecking and elaboration for STλC, and from
there, we build two other variations, Bidirectional STλC and Search-based Type
Inference, to showcase the versatility of our framework. Our results are implemented
in Agda.
location: LT1414a and Online
material: []
- tag: CancelledTalk
date: '2024-12-13T13:00:00Z'
speaker: Neil Ghani
speakerurl: ''
institute: MSP
insturl: ''
title: Scientific anarchy
abstract: TBD
location: LT412 and Online
material: []
- tag: CancelledTalk
date: '2024-12-13T13:00:00Z'
speaker: Clemens Kupke
speakerurl: ''
institute: MSP
insturl: ''
title: Parity Formulas
abstract: In this talk, I will discuss how modal mu-formulas can be succinctly represented
as graphs, thus avoiding some of the variable naming issues that Sean sketched
in his recent 101. A key technical problem when switching to graphs is that the
natural dependency order between fixpoint operators is obfuscated. Therefore our
graphs need to be equipped with a parity function that encodes this order. We
call the resulting graphs with parity functions <q>parity formulas</q>. This is
based on joint work with Johannes Marti and Yde Venema.
location: LT511 and Online
material: []
- tag: Talk
date: '2024-11-29T13:00:00Z'
speaker: Fredrik Nordvall Forsberg
speakerurl: ''
institute: MSP
insturl: ''
title: 'Data type science: how to reason about classes of data types in type theory'
abstract: Different proof assistants and programming languages have different notions
of data types. Sometimes this means that we can prove more theorem in one system
compared to another, and sometimes it only means that one system is more convenient
to use. How can we tell the difference? I'll give an introduction to how we can
represent and reason about classes of data types in type theory, and I'll show
some examples from the zoo of classes that have been considered.
location: LT210 and Online
material: []
- tag: CancelledTalk
date: '2024-11-22T13:00:00Z'
speaker: Danielle Marshall
speakerurl: ''
institute: University of Glasgow
insturl: ''
title: TBC
abstract: TBC
location: LT412 and Online
material: []
- tag: Talk
date: '2024-11-15T13:00:00Z'
speaker: Jade Master
speakerurl: https://sites.google.com/view/jadeedenstarmaster
institute: GLAIVE
insturl: ''
title: Representation Matters (Taking Categories Seriously)
abstract: When we endeavor to build software based on category theory, we often
have two categorically equivalent structures that represent the same underlying
data and the correct choice of structure subtly depends on what you would like
to do. The first generation of categorical programming languages heavily used
the monad to represent algebraic effects. However, what if we made a different
choice? Categorically equivalent to Monads are Lawvere theories, whose presentation
as categories allows for many useful constructions which are more awkward in the
Monad representation. In this talk, I will imagine what a system for algebraic
effects based on Lawvere theories might look like. This talk will include a lightning
introduction to Lawvere theories as well as a tour through an idris2 implementation
of these ideas which still contains too many holes to float.
location: LT310 and Online
material:
- tag: Link
address: https://youtu.be/FlOWErswJzw
linkDescription: Video
- tag: Link
address: https://gitlab.com/glaive-research/lawvereeffects
linkDescription: Code
- tag: Talk
date: '2024-11-08T13:00:00Z'
speaker: Bob Atkey
speakerurl: ''
institute: MSP
insturl: ''
title: How to Make Good Choices
abstract: What to do? One way to find out is to explore all the consequences of
our choices and pick the best one. Or we could assume we have a magic device that
tells us what the outcome of our choice will be, and to pick the best one straight
off. In terms of programming, the former can be modelled using a monad for non-deterministic
choices and the latter using the Selection monad of Escardo and Oliva. I'll relate
these two monads via a logical relation, showing that if we are careful to respect
abstraction boundaries, the two are equivalent for closed programs. I'll then
extend this correspondence to account for different kinds of choice-making program
and see how we can reconstruct concepts like Nash equilibrium. This talk may involve
some live coding in Agda.
location: LT210 and Online
material:
- tag: Link
address: https://youtu.be/8ueFihu8Ja8
linkDescription: Video
- tag: Link
address: https://gist.github.com/bobatkey/b9ba09a9934bed48ae3551493173f952
linkDescription: Agda code
- tag: Talk
date: '2024-11-01T13:00:00Z'
speaker: Guillaume Allais
speakerurl: ''
institute: MSP
insturl: ''
title: Partial evaluation
abstract: Partial evaluation shows up all across PL in compilation (optimization),
meta-theory (normalization), and code-generation (staging). I will give a gentle
introduction to partial evaluation using semantic methods, showing how we can
strategically build different models to decide different equational theories.
This will be an Agda-mediated live coding show.
location: LT309 and Online
material:
- tag: Link
address: https://youtu.be/O-bHGWL7PNY
linkDescription: Video
- tag: Talk
date: '2024-10-28T14:00:00Z'
speaker: Sean Watters
speakerurl: ''
institute: MSP
insturl: ''
title: The Madness of the Modal μ-Calculus
abstract: In this talk, I'll give you the <q>what</q>, <q>why</q>, and <q>how</q>
of the μ-calculus - what it is, why I find it interesting (and hopefully why
you should too!), and how to tame it in Agda. </p>I'll start by introducing and
motivating the field of model checking, before quickly diverting to the modal
μ-calulus, a fixpoint modal logic of foundational importance in that field.
I'll talk about its semantics first, because that's only sensible, then the rest
of the talk will be devoted to the weird and wonderful (but mostly weird) syntactic
issues that arise from this formalism. In particular, I'll focus on an important
syntactic construction called <q>the closure</q> of a μ-calculus formula, which
is not stable under alpha-equivalence, and whose inductive structure is somewhat
non-obvious. </p>In the second half, we'll code up an implementation of the μ-calculus
in Agda, which will also serve as an introduction to well-scoped De Bruijn syntax.
I'll work towards defining parallel substitution and weakening, and finish with
the definition of the closure, and a (very) brief sketch of its correctness proof.
The data type of thinnings between natural numbers will feature.</p>If there's
time (which there probably won't be), I'll discuss an extension of well-scoped
De Bruijn syntax that I've been calling <q>sublimely-scoped</q> syntax, which
is still very WIP.
location: LT310 and Online
material:
- tag: Link
address: https://youtu.be/opJpkKgP288
linkDescription: Video
- tag: Talk
date: '2024-10-18T13:00:00Z'
speaker: Clovis Eberhart
speakerurl: ''
institute: MSP
insturl: ''
title: A Compositional Approach to Verification Models
abstract: We will present a compositional approach to graph-like verification models
(e.g., parity games, Markov decision processes, or Petri nets) based on <q>open</q>
structures. Such open structures are graphs with potentially dangling edges called
<q>open ends</q>, and which form interfaces along which open structures can be
composed. We thus define a syntactic category of interfaces and open structures
between them. We then define a semantic category representing relevant information
about the structure (e.g., a category of probabilistic rewards). Finding an interpretation
functor from the syntactic category to the semantic one shows that these structures'
semantics can be computed compositionally. (This is joint work with Kazuki Watanabe,
Kazuyuki Asada, Ichiro Hasuo, and Serge Lechenne.)
location: LT714 and Online
material:
- tag: Link
address: https://youtu.be/FRBpabpuBGE
linkDescription: Video
- tag: Talk
date: '2024-10-11T13:00:00Z'
speaker: Jan de Muijnck-Huges
speakerurl: ''
institute: MSP
insturl: ''
title: Bidirectional Typing & Session Types, A Beautiful Friendship?
abstract: Session Types are a neat typing discipline to reason both statically and
dynamically about program interaction. An interesting question is how best we
should check communicating programs against a given global type.</p>Bidirectional
typing is an important technique for programming language design and implementation,
enabling us to transform the theory of how we should check the type of a term
and incorporate the practice of inferring the term's type.</p>This talk serves
as a gentle introduction to bidirectional type system design and session types,
and how combining the two can help make type checking session typed programs that
little bit easier.
location: LT714 and Online
material: []
- tag: Talk
date: '2024-10-04T13:00:00Z'
speaker: André Videla
speakerurl: ''
institute: MSP
insturl: ''
title: Cooking with Proofs
abstract: The Curry-Howard correspondence says that types are propositions and programs
are proofs. But what proof is Super Mario World on the SNES? In this introductory
presentation we'll explore how the Curry-Howard correspondence manifests in different
programming environments and how to employ it for software development.
location: LT210 and Online
material: []
- tag: Talk
date: '2024-09-27T13:00:00Z'
speaker: Conor McBride
speakerurl: ''
institute: MSP
insturl: ''
title: Effing W
abstract: I shall revisit the Hindley-Milner type system for the traditional Core
ML (old sense) language of variables, application, monomorphic abstraction and
polymorphic definition, to give a new twist on its implementation. In particular,
I shall consider the role that the context plays in the type inference process,
and then make it disappear, replacing context-as-data-structure with context-as-control-structure,
demonstrating the power of effects and handlers. The extra ingredient which gives
this new recipe its spice is to index with respect to a suitably compositional
notion of "progress". I shall make that disappear, too!
location: LT210 and Online
material: []
- tag: SpecialEvent
date: '2024-09-20T13:00:00Z'
endDate: '2024-09-20T14:00:00Z'
title: MSP101 Planning meeting
url: ''
location: LT1310 and Online
locationurl: ''
description: ''
- tag: Talk
date: '2024-04-17T13:00:00Z'
speaker: Dov M. Gabbay
speakerurl: https://en.wikipedia.org/wiki/Dov_Gabbay
institute: Augustus De Morgan Professor Emeritus of Logic, King's College London
insturl: ''
title: Intro to argumentation
abstract: This is a blackboard talk introducing the audience to argumentation.
location: LT11, boardroom
material: []
- tag: Talk
date: '2024-02-13T12:00:00Z'
speaker: Nobuko Yoshida
speakerurl: https://mrg.cs.ox.ac.uk/people/nobuko-yoshida/
institute: Strachey Chair at University of Oxford
insturl: ''
title: Session types, Linear Logic and Expressiveness
abstract: |-
I will first talk about the origin of session types and its relationship with expressiveness.
The first technical part of this talk will present an expressiveness result between Linear Logic-based Session Types and System F. The second part gives a summary of recent results on session types, highlighting the expressiveness correspondence between various session-based process calculi.
location: LT412
material: []
- tag: SpecialEvent
date: '2024-05-03T15:00:00Z'
endDate: '2024-05-03T16:00:00Z'
title: Academic Promotion Information Meeting
url: ''
location: LT209 (TBC)
locationurl: ''
description: ''
- tag: SpecialEvent
date: '2024-03-29T15:00:00Z'
endDate: '2024-03-29T16:00:00Z'