Homepage of Jonas Frey

I am currently postdoc at Carnegie Mellon University in Pittsburgh.

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

Publications

• Triposes, q-toposes and toposes, Annals of Pure and Applied Logic 166.2 (2015): 232-259.
• Realizability toposes from specifications, TLCA 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.

Notes, Preprints

• A 2-categorical analysis of the tripos-to-topos construction
• 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)
• Realizability toposes as homotopy categories

Slides of some talks

• 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
• An invitation to toposes, Séminaire des Thésards LIAFA/PPS, October 2008, Paris, France

My PhD thesis

• A fibrational study of realizability toposes

My master thesis

• A Universal Characterisation of the Tripos-to-Topos Construction