Szumi Xie [ˈsʊmɪ ɕêɛ̯] (they/them)

I’m a PhD student in the Budapest Type Theory Group at Eötvös Loránd University (ELTE) in Budapest, Hungary, supervised by Ambrus Kaposi.

Papers

• The groupoid-syntax of type theory is a set

  with Thorsten Altenkirch and Ambrus Kaposi

  CSL 2026

  PDF · repository · highlighted code

• The conatural numbers form an exponential commutative semiring

  with Viktor Bense

  TyDe 2025

  PDF · repository

• Type theory with single substitutions

  with Ambrus Kaposi

  LFMTP 2025

  PDF · repository · highlighted code

• Second-order generalised algebraic theories: signatures and first-order semantics

  with Ambrus Kaposi

  FSCD 2024

  PDF · repository

Talks

• The groupoid-syntax of type theory is a set

  HoTTEST (2026), online

  slides · video

• The conatural numbers form an exponential commutative semiring

  TyDe 2025, Singapore

  slides · video

• Type theory with single substitutions

  LFMTP 2025, Birmingham

  slides

• Conatural numbers in Cubical Agda

  Agda Implementors’ Meeting XL (2025), Budapest

  Agda file 1 · Agda file 2

• Second-order generalized algebraic theories (logic edition)

  World Logic Day 2025, Budapest

  abstract · slides

• Second-order generalised algebraic theories (lightning edition)

  SPLV 2024 lightning talk, Glasgow

  slides

• Second-order generalised algebraic theories: signatures and first-order semantics

  FSCD 2024, Tallinn

  slides

• Type theory in type theory using single substitutions

  TYPES 2024, Copenhagen

  abstract · slides

• A model of type theory supporting quotient inductive-inductive types

  Developments in Computer Science (2021), Budapest (online)

  abstract · slides

• A model of type theory with quotient inductive-inductive types

  TYPES 2020, Turin (cancelled)

  abstract · slides

Notes

• CCwFs vs. comprehension categories