Homepage of Jonas Frey

I'm maître de conférences in the Équipe LoCal of the Laboratoire d'Informatique de Paris Nord at the Université Sorbonne Paris Nord.

Below you can find my publications and preprints, and some slides and recordings of talks. Please let me know if you find dead or incorrect links.

News

• I'm on the program committees of HoTT/UF 2025 (15–16 April 2025, in Genoa, Italy), and ACT 2025 (June 2-6, 2025 in Gainesville, Florida).

• In December 19, 2024, I gave a talk at the Workshop on Categorical Logic and Higher Categories in Manchester.

• From June 10 to 14, 2024, I was co-teaching a course on Categorical Semantics and Synthetic Topology with Reid Barton at the Summer School in Logic and Formal Epistemology at Carnegie Mellon University.

• I was on the local committee of the Homotopy Type Theory 2023 conference, which took place at Carnegie Mellon University in Pittsburgh between May 22 and May 25, 2023.

• I was invited speaker at the Workshop on Doctrines & Fibrations which took place at the Department of Mathematics “Tullio Levi-Civita” in Padova from May 29 to June 1, 2023.

Publications

• Preprint (accepted in TAC): Uniform Preorders and Partial Combinatory Algebras (2024)

• Preprint (accepted in JSL): Duality for Clans: an Extension of Gabriel-Ulmer Duality (2023)

• Constructing Coproducts in locally Cartesian closed ∞-Categories (with Nima Rasekh), Homotopy, Homology and Applications (2023)

• Categories of partial equivalence relations as localizations, Journal of Pure and Applied Algebra (2023)

• Triposes as a generalization of localic geometric morphisms (with Thomas Streicher), Mathematical Structures in Computer Science (2021)

• Characterizing partitioned assemblies and realizability toposes, Journal of Pure and Applied Algebra (2019)

• Impredicative Encodings of (Higher) Inductive Types (with Steve Awodey and Sam Speight), Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (2018), Lean code

• Ordered combinatory algebras and realizability (with Walter Ferrer Santos, Mauricio Guillermo, Octavio Malherbe and Alexandre Miquel), Mathematical Structures in Computer Science (2017)

• Classical realizability in the CPS target language, Electronic Notes in Theoretical Computer Science (2016)

• Realizability toposes from specifications, Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications (2015)

• Triposes, q-toposes and toposes, Annals of Pure and Applied Logic (2015)

Unpublished Notes

• Notes of a categorical logic course at CMU in 2017

• A 2-categorical analysis of the tripos-to-topos construction. A complete rewrite of this, which is much shorter, and unfortunately doesn't contain any string diagrams, was published under the title "Triposes, q-toposes, and toposes", see above. 

• Toposes for Time Complexity Classes (with Jakob Grue Simonsen, presented at DICE 2016)

• Confluence and strong normalization for the CPS target language (presented at HOR 2016)

• Notes on 2-categorical limits (notes of a seminar talk in February 2010 at Paris 7 University)

• Computability and Krivine realizability (based on a conversation with J.-L. Krivine in November 2015)

Some Slides and Videos

• Modest sets and equilogical spaces as mono-fibrational cocompletions , LHC and IDIA days 2025 June 2025, Palaiseau, France.

• Characterizing realizability triposes over PCAs, CIRM Realizability Workshop, April 2025, Marseille Luminy, France

• Partial equivalence relations, localizations, and equipments,  Workshop on Doctrines and Fibrations, May 2023, Padova, Italy, Video 

• Basic Combinatory Objects, Uniform Preorders and Partial Combinatory Algebras, Category Theory Octoberfest 2022, Video 

• An Introduction to Cohesive Homotopy Type Theory, HoTT special session at the  ASL 2022 North American Annual Meeting

• Characterizing clan-algebraic categories, Homotopy Type Theory Electronic Seminar Talks series, February 2022, Video 

• Coproducts in ∞-LCCCs with subobject classifier, HoTT/UF 2021, July 2021, Video Conference, Video 

• A refinement of Gabriel-Ulmer duality, HoTT/UF 2020, July 2020, Video Conference

• A language for closed cartesian bicategories, CT 2019, July 2019, Edinburgh, Scotland

• Modelling homotopy type theory in cartesian cubical sets, CT 2017, Vancouver, Canada

• Classical realizability in the CPS target language, Realizability in Uruguay 2016, July 2016, Piriapolis, Uruguay

• Realizability toposes as homotopy categories, Topos à l'IHES, November 2015, Bures-sur-Yvette, France

• Realizability toposes from specifications, TLCA 2015, July 2015, Warsaw, Poland

• Enriched triposes and enriched Pitts functors, PSSL 96, October 2014, Palermo, Italy

• Characterizing realizability toposes, CT 2014, June 2014, Cambridge, England

• Moens’ theorem and fibered toposes, ScotCats 9: Fibrations in Computation Workshop, June 2014, Glasgow, Scotland

• A fibrational analysis of realizability toposes, Slides of my PhD defense, June 2013, Paris, France

• Indexed preorders, uniform preorders, and PCAs, Réalisabilité à Chambéry #5, June 2012, Chambéry, France

• Multiform preorders and partial combinatory algebras, Logic and interactions 2012, February 2012, Marseilles, France

• A double categorical analysis of the tripos-to-topos construction, CT 2010, June 2010, Genoa, Italy

My PhD Thesis

• A fibrational study of realizability toposes, supervised by Paul-André Melliès at Paris 7 University (now Université Paris Cité)

My Master's Thesis

• A Universal Characterisation of the Tripos-to-Topos Construction, supervised by Thomas Streicher at Darmstadt University