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.
Schedule
| Date | Topic |
|---|---|
| ??? | Bindings as Bounded Natural Functors (Blanchette et al, POPL 19) |
| 2022-10-07 09:30 | On Imperative Session Types |
| 2022-09-23 10:00 | Semantic preservation for a type directed translation scheme of Featherweight Go |
| 2022-05-20 09:30 | Productive coprogramming with guarded recursion (McBride and Atkey, ICFP 13) |
| 2022-04-29 14:00 | An Introduction to Logical Relations (Amal Ahmed, Lecture Notes, OPLSS 16) |
| 2022-02-18 09:30 | Trees that grow (Najd, Peyton Jones) |
| 2022-02-11 09:30 | An existential crisis resolved: type inference for first-class existential types (Eisenberg et al, ICFP 21) |
| 2022-02-04 09:30 | symbolic execution... (Torlak et al, POPL 22) |
| 2022-01-28 09:30 | Bachelorthesis presentation: Janek Spaderna |
| 2022-01-21 09:30 | Survey on bidirectional typing (Dunfield, Krishnaswami, CS) |
| 2021-12-10 09:30 | Separation Logic for Sequential Programs (Charguéraud, ICFP2020) |
| 2021-12-03 09:30 | Separation Logic for Sequential Programs (Charguéraud, ICFP2020) |
| 2021-11-26 09:30 | Relational Nullable Types with Boolean Unification (Madsen, Van de Pol) |
| 2021-11-12 09:30 | Compiling 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:30 | Build Scripts with Perfect Dependencies with video |
| 2021-03-29 11:30 | Build systems a la carte |
| 2021-03-22 11:30 | Build systems a la carte |
| 2021-03-15 11:30 | Chapman, Kireev, Nester, Wadler System F in Agda for Fun and Profit |
| 2021-03-09 09:00 | Chapman, Kireev, Nester, Wadler System F in Agda for Fun and Profit |
| 2021-02-04 14:00 | Mokhov, Lukyanov, Marlow, Dimino. Selective Applicative Functors, video (Haskell2019) |
| 2021-01-26 15:30 | Bembenek, Greenberg, Chong. 2020. Formulog: Datalog for SMT-Based Static Analysis |
| 2020-12-22 16:00 | Chapman, Dagand, McBride, Morris. The Gentle Art of Levitation |
| 2020-12-15 16:00 | Allais et al. A type and scope safe universe of syntaxes with binding: their semantics and proofs |
| 2020-12-08 17:00 | Allais et al. A type and scope safe universe of syntaxes with binding: their semantics and proofs |
| 2020-12-01 17:00 | Connor McBride. Type-Preserving Renaming and Substitution |
| 2020-11-10 10:00 | James Wood and Robert Atkey. A Linear Algebra Approach to Linear Metatheory |
| 2020-11-03 16:00 | more Profunctor Optics |
| 2020-10-30 10:00 | John 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:00 | Matthew 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-07 | Guillaume 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:00 | Bachelor project Fabian Krause |
| 2020-09-22, 2020-09-30 | Representable Functors |
| 2020-09-15 | Yoneda Lemma |
| 2020-09-09 | Sparcl, a Language for Partially Invertible Computation (ICFP 2020) |
| 2020-09-01 | Safer Smart Contract Programming with Scilla (OOPSLA 2019) |
| 2020-08-26 | A 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