Works

Papers

Talks

A Metatheoretic Analysis of Subtype Universes

28/07/2023
Felix BradleyZhaohui Luo
Published in Post-proceedings of TYPES 2022 in Leibniz International Proceedings in Informatics
paperdoierrata
#type theory#coercive subtyping#subtype universes

Talks

Papers

Weak Equality Reflection in MLTT with Propositional Truncation

09/07/2025 - 13/07/2025
Felix BradleyZhaohui Luo
Presented at TYPES 2025 in Glasgow, Scotland
ext. abstractslides
#type theory#coercive subtyping#natural language semantics#propositional truncation#homotopy type theory

Representing Temporal Operators with Dependent Event Types

10/07/2024 - 14/07/2024
Felix BradleyZhaohui Luo
Presented at TYPES 2024 in Copenhagen, Denmark
ext. abstractslides
#type theory#coercive subtyping#natural language semantics#dependent event types

An Introduction to Type Theory

28/02/2024
Felix Bradley
Presented at Department of Mathematics in Royal Holloway, University of London, UK
slides
#type theory

On the Metatheory of Subtype Universes

11/07/2023 - 14/07/2023
Felix BradleyZhaohui Luo
Presented at TYPES 2023 in Valencia, Spain
ext. abstractslides
#type theory#coercive subtyping#subtype universes

On the Metatheory of Subtype Universes

23/04/2023 - 24/04/2023
Felix BradleyZhaohui Luo
Presented at EuroProofNet Working Group 6 Meeting in Vienna, Austria
slides
#type theory#coercive subtyping#subtype universes