Szumi Xie [ˈsʊmɪ ɕêɛ̯]

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

  (PDF, highlighted code)

• The conatural numbers form an exponential commutative semiring

  with Viktor Bense

  accepted to TyDe 2025

  (repository)

• Type theory with single substitutions

  with Ambrus Kaposi

  accepted to LFMTP 2025

  (repository, highlighted code)

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

  with Ambrus Kaposi

  FSCD 2024

  (PDF, repository)

Talks

• 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)

  7th 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)