Homepage of Jonas Frey
I am a postdoc in the Homotopoy Type Theory research group at Carnegie Mellon University in Pittsburgh.
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.
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.
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.
Triposes, q-toposes and toposes, Annals of Pure and Applied Logic 166.2 (2015): 232-259.
Realizability toposes from specifications, Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, 2015: 196-210.
Classical realizability in the CPS target language, Electronic Notes in Theoretical Computer Science 325 (2016): 111-126.
Ordered combinatory algebras and realizability (with Walter Ferrer Santos, Mauricio Guillermo, Octavio Malherbe and Alexandre Miquel), Mathematical Structures in Computer Science 27.3 (2017): 428-458.
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. ACM, 2018, Lean code
Characterizing partitioned assemblies and realizability toposes, Journal of Pure and Applied Algebra 223.5 (2019): 2000-2014.
Triposes as a generalization of localic geometric morphisms (with Thomas Streicher), Mathematical Structures in Computer Science, 2021
Categories of partial equivalence relations as localizations, Journal of Pure and Applied Algebra, 2022
Constructing Coproducts in locally Cartesian closed ∞-Categories (with Nima Rasekh), accepted in Homotopy, Homology and Applications
A 2-categorical analysis of the tripos-to-topos construction. A complete rewrite of this, which is much shorter, was published under the title "Triposes, q-toposes, and toposes", see above.
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
Partial equivalence relations, localizations, and equipments, Workshop on Doctrines and Fibrations, May 2023, Padova, Italy, Video
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
A fibrational analysis of realizability toposes, Slides of my PhD defense, June 2013, Paris, 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