Skip to content

Home

Jump to bottom
Fabian edited this page Feb 2, 2022 · 458 revisions

Initial Types Club

We (usually) meet on Thursdays between 16:00 and 17:30 both in room 8103 (on the 8th floor of the EDIT building) and on Zoom.

About ITC: https://initialtypes.github.io/Club/

Mailing list: [email protected] (subscribe to receive announcements, archive)

Schedule of the academic year 2021/22

LP3/4 (Jan–Jun 2022):

Date Leader Topic Remark
3 Feb Peter Martin-Löf's Meaning Explanations
10 Feb Matthew Daggit Designing a Language for Machine-Learning Verfication TBC (Warrick)
17 Feb Warrick Backprop as Functor TBC (Warrick)
17 Mar Tentamensvecka
24 Mar Läsperiod 4
2 Jun Tentamensvecka
27 Jan
20 Jan Läsperiod 3

LP1/2 (Sep–Dec 2021):

Date Leader Topic Remark
13 Jan Tentamensvecka
16 Dec–6 Jan
9 Dec Szumi Xie Quotient Inductive-Inductive Types Analysen
2 Dec Thierry Canonicity and Normalization for Type Theory Analysen
25 Nov Andreas On Consistency, Models, and Normalization for IPL
18 Nov Carlos Hackathon: Implementing Normalization-by-Evaluation
11 Nov Carlos Normalization-by-Evaluation by Example
4 Nov Nachi Reduction-based Normalization Läsperiod 2
28 Okt Tentamensvecka
21 Okt Carlos Normalization-by-Evaluation by Example Uppskjuten
7–14 Okt
30 Sep Carlos and Nachi STLC–CCC (Part III)
23 Sep Andreas STLC–CCC (Part II)
16 Sep Sandro STLC–CCC (Part I)
13–14 Sep Proof and Computation
9 Sep Warrick On the Grammar of Proof MSc thesis
2 Sep Läsperiod 1

Topics and suggestions

Topic collection from first brain storming session 2017-11-22:

  • Normalization
  • Logical Relations
  • Parametricity (invite Jean-Philippe)
  • Moggi's Computational Lambda Calculus and Monads (Sandro's abstract)
  • How to formalize stuff in Agda (Jesper's abstract)
  • Session types
  • Homotopy type theory
  • Cubical type theory
  • Foundations of mathematics
    • Set theory (Mattias' notes)
    • Type theory (calculus of constructions) (Thierry's abstract)
    • Category theory
  • What is "computational content"?
    • Models using computable functions
    • Realizability models
  • Intuitionistic vs. classical logic
  • Reflection in Agda (invite Ulf)
  • How to write a paper with literate Agda
  • Functors, natural transformations, F-algebras, inductive types and folds.
  • Tree automata (Folkmar gave a lecture)

New topics added on 15/03/2018:

  • Logical framework and higher-order abstract syntax (Twelf)
  • Dependent type theory (mathematical presentation, judgements and rules) (Konstantinos)
  • Logical relations and normalization for dependent types (AA)
  • Pure type systems and the lambda-cube, (im)predicativity
  • Categories: presheaves
  • Frederik HI's master thesis: Univalent categories
  • Syntax and semantics of inductive data types / sized types
  • Motivations for HoTT and Univalent foundations (Thierry?)
  • Contributing to agda/agda and agda/agda-stdlib

New topics added on 31/05/2018:

  • Kripke semantics (following Aaron Stump's Agda book, Andreas' repo, Frederik's abstract)
  • Initiality of CwF in cubical Agda (Andreas K)
  • Higher inductive types (Andrea?)
  • (Categorical) models of type theory
    • set models
    • (split, full) comprehension categories (Christian presented locally cartesian closed categories)
    • categories with attributes
    • categories with families (CwF's)/natural models/functorial semantics of type theories à la Uemura (Peter's abstract, Konstantinos' code)
    • contextual categories
    • ...
    • tribes/type-theoretic fibration categories
  • Topoi (David)
  • Higher-order unification (Víctor?)
  • The Yoneda Embedding (Jannis' abstract)
  • Adjoints

New topics on 13/09/2018:

  • Formal biology (Sandro)
  • Inductive and coinductive types, (co)pattern matching (Jesper)
  • Type intervals and subtyping (Sandro)
  • Polarities in type theory (Sandro or Andreas A)
  • Sized types: practice/tutorial + theory (in that order (according to Sandro)) (Andreas or Andrea)
  • Beta-eta equality for coproducts and the empty type (Andreas?)

New topics on 26/09/2019:

  • Induction recursion (invite Peter Dybjer)
  • NbE and Partial Evaluation (Peter Dybjer/Andreas Abel)

New topics on 16/01/2020:

  • Partiality and general recursion in type theory (Ana's abstract)
  • Abstract interpretation (Matthías' abstract)
  • Semantic completeness for modal and intuitionistic logic
  • Team semantics for dependence logic (invite Irene)
  • Fixpoints of functors, F-algebras/algebras for endofunctors, inductive types and folds (invite Patrik)
  • Linear types (invite Jean-Philippe)
  • Classical proofs as programs: Parigot's lambda-mu calculus, continuation semantics
  • Monadic reflection ("bridge between value and behaviour views of computational effects"), and delimited continuations
  • Nominal sets, and their logic for freshness, abstraction and scoping of bound names
  • Some group theory as the theory of pointed connected groupoids in HoTT/UF
  • Domain-theoretic foundations of functional programming: The Scott model of PCF (Programming Computable Functionals)
  • Games…emantics
  • "Reynolds programme for category theory and programming languages" (logical relations and parametricity)
  • Correspondences between theories (internal language) and models (syntactic model):
    • Curry-Howard-Lambek-Correspondence, STLC and CCCs in Agda (Andreas' abstract, notes (part I), notes (part II), and code)
    • extensional MLTT and LCCCs
    • first-order theories and hyperdoctrines
    • higher-order theories and elementary toposes
    • intensional MLTT with dependent sums and finitely complete (∞,1)-categories
    • homotopy type theory and "elementary (∞,1)-toposes"
  • Canonicity, normalization, parametricity, decidability of conversion via sconing/Artin glueing/Freyd covers (logical relations)

Previous schedules

Clone this wiki locally