Skip to content

Home

Jump to bottom
Fabian edited this page Dec 5, 2022 · 458 revisions

Initial Types Club

The previous academic year ended on Sunday, June 5th — välkommen tillbaka!

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

Mailing list: initial-types@lists.chalmers.se (subscribe to receive announcements, archive)

Schedule of the academic year 2022/23

Date Leader Topic Remark
10 Nov AIMXXXI
20 Oct–3 Nov
6 Oct–13 Oct Types, Thorsten and Theories
29 Sep Proof and Computation
1 Sep–22 Sep

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