Oberseminar Arbeitsbereich Programmiersprachen

Time and Date:
TBD, online

Oberseminar Programmiersprachen is a weekly meeting for members and friends of the group to discuss (mostly new) research papers on programming languages and related topics. Typicially, participants study the paper before the meeting, during the meeting we discuss questions and interesting aspects of the paper. Everyone interested in programming languages research is welcome.

Moreover, final presentations of projects, bachelor theses, and master theses take place in the Oberseminar. There are also presentations of new research taking place in the group.

Time, Date, and Location

We generally meet via video conference. If you are interested in joining us, feel free to write an email to thiemann@info... and ask for an invite link.

The time, date, and topic of the next meeting may be found in the schedule below.


???Bindings as Bounded Natural Functors (Blanchette et al, POPL 19)
2022-10-07 09:30On Imperative Session Types
2022-09-23 10:00Semantic preservation for a type directed translation scheme of Featherweight Go
2022-05-20 09:30Productive coprogramming with guarded recursion (McBride and Atkey, ICFP 13)
2022-04-29 14:00An Introduction to Logical Relations (Amal Ahmed, Lecture Notes, OPLSS 16)
2022-02-18 09:30Trees that grow (Najd, Peyton Jones)
2022-02-11 09:30An existential crisis resolved: type inference for first-class existential types (Eisenberg et al, ICFP 21)
2022-02-04 09:30symbolic execution... (Torlak et al, POPL 22)
2022-01-28 09:30Bachelorthesis presentation: Janek Spaderna
2022-01-21 09:30Survey on bidirectional typing (Dunfield, Krishnaswami, CS)
2021-12-10 09:30Separation Logic for Sequential Programs (Charguéraud, ICFP2020)
2021-12-03 09:30Separation Logic for Sequential Programs (Charguéraud, ICFP2020)
2021-11-26 09:30Relational Nullable Types with Boolean Unification (Madsen, Van de Pol)
2021-11-12 09:30Compiling with Continuations, Correctly (Paraskevopoulou, Grover)
2021-10-22 09:30 Quantitative Type Theory (Robert Atkey)
2021-10-14 09:30 Quantitative Type Theory (Robert Atkey)
2021-10-07 09:00 A General Lattice Model for Merging Symbolic Execution Branches
... ...
2021-05-03 11:30 Presentation Bachelor Thesis Fabian Krause
2021-04-26 11:30 Presentation Bachelor Project Janek Spaderna
2021-04-19 11:30 Staged Selective Parser Combinators (ICFP 2020)
2021-04-12 11:30Build Scripts with Perfect Dependencies with video
2021-03-29 11:30Build systems a la carte
2021-03-22 11:30Build systems a la carte
2021-03-15 11:30Chapman, Kireev, Nester, Wadler System F in Agda for Fun and Profit
2021-03-09 09:00Chapman, Kireev, Nester, Wadler System F in Agda for Fun and Profit
2021-02-04 14:00Mokhov, Lukyanov, Marlow, Dimino. Selective Applicative Functors, video (Haskell2019)
2021-01-26 15:30Bembenek, Greenberg, Chong. 2020. Formulog: Datalog for SMT-Based Static Analysis
2020-12-22 16:00Chapman, Dagand, McBride, Morris. The Gentle Art of Levitation
2020-12-15 16:00Allais et al. A type and scope safe universe of syntaxes with binding: their semantics and proofs
2020-12-08 17:00Allais et al. A type and scope safe universe of syntaxes with binding: their semantics and proofs
2020-12-01 17:00Connor McBride. Type-Preserving Renaming and Substitution
2020-11-10 10:00James Wood and Robert Atkey. A Linear Algebra Approach to Linear Metatheory
2020-11-03 16:00more Profunctor Optics
2020-10-30 10:00John C. Reynolds and Gordon D. Plotkin. 1993. On Functors Expressible in the Polymorphic Typed Lambda Calculus. Inf. Comput. 105, 1 (1993), 1–29.
2020-10-27 14:00Matthew Pickering, Jeremy Gibbons, Nicolas Wu. Profunctor Optics: Modular Data Accessors. The Art, Science, and Engineering of Programming, 2017, Vol. 1, Issue 2, Article 7.
2020-10-20 14:00(continue) and R.S. Bird. 1984. The Promotion and Accumulation Strategies in Transformational Programming. TOPLAS 6, 4 (1984), 487-504.
2020-10-07Guillaume Boisseau, Jeremy Gibbons: What you needa know about Yoneda: profunctor optics and the Yoneda lemma (functional pearl). Proc. ACM Program. Lang. 2(ICFP): 84:1-84:27 (2018) href
2020-10-12 11:00Bachelor project Fabian Krause
2020-09-22, 2020-09-30Representable Functors
2020-09-15Yoneda Lemma
2020-09-09Sparcl, a Language for Partially Invertible Computation (ICFP 2020)
2020-09-01Safer Smart Contract Programming with Scilla (OOPSLA 2019)
2020-08-26A Unified View of Modalities in Programming Languages (ICFP 2020)

If there is an entry denoting a person, then that person is responsible to provide a link to the paper one week before the date.

Future Topics

  • A. Díaz-Caro, P. E. Martínez López. Isomorphisms considered as equalities
  • C. F. Sottile, A. Díaz-Caro, P. E. Martínez López. Polymorphic System I
  • E. S. Bainbridge, Peter J Freyd, Andre Scedrov, and Philip J. Scott. 1990. Functorial Polymorphism. Theor. Comput. Sci. 70, 1 (1990), 35–64. https://doi.org/10.1016/0304-3975(90)90151-7
  • N. P. Mendler. 1987. Recursive Types and Type Constraints in Second-Order Lambda Calculus. In Proceedings of the Symposium on Logic in Computer Science (LICS ’87), Ithaca, New York, USA, June 22-25, 1987. 30–36.
  • Separation Logic for Sequential Programs (ICFP 2020)
  • Purity for Comonads (ICFP 2020)
  • Parsing with Zippers (ICFP 2020)
  • Kinds as Calling Conventions (ICFP 2020)
  • Exploiting the Laws of Order in Smart Contracts (ISSTA 2019)
  • Actris, POPL 2020
  • Partially-Static Data as Free Extension of Algebras, ICFP 2018, paper