### On indefinite truth values

- 13 August 2023
- Logic

In a discussion following a MathOverflow answer by Joel Hamkins, Timothy Chow and I got into a chat about what it means for a statement to “not have a definite truth value”. I need a break from writing the paper on countable reals (coming soon in a journal near you), so I thought it would be worth writing up my view of the matter in a blog post.

→ continue reading### Variations on Weihrauch degrees (CiE 2023)

- 28 July 2023
- Talks, Computation

I gave a talk “Variations on Weihrauch degrees” at Computability in Europe 2023, which took place in Tbilisi, Georgia. The talk was a remote one, unfortunately. I spoke about generalizations of Weihrauch degrees, a largely unexplored territory that seems to offer many opportunities to explore new directions of research. I am unlikely to pursue them myself, but will gladly talk with anyone who is interested in doing so.

**Slides:** `CiE-2023-slides.pdf`

.

### Continuity principles and the KLST theorem

- 19 July 2023
- Constructive math, Synthetic computatibility

On the occasion of Dieter Spreen's 75th birthday there will be a Festschrift in the Journal of Logic and Analysis. I have submitted a paper *“Spreen spaces and the synthetic Kreisel-Lacombe-Shoenfield-Tseitin theorem”*, available as a preprint arXiv:2307.07830, that develops a constructive account of Dieter's generalization of a famous theorem about continuity of computable functions. In this post I explain how the paper fits into the more general topic of continuity principles.

### Isomorphism invariance and isomorphism reflection in type theory (TYPES 2023)

- 15 June 2023
- Talks, Type theory

At TYPES 2023 I had the honor of giving an invited talk “On Isomorphism Invariance and Isomorphism Reflection in Type Theory” in which I discussed isomorphism reflection, which states that isomorphic types are judgementally equal. This strange principle is consistent, and it validates some fairly strange type-theoretic statements.

Here are **the slides with speaker notes** and **the video recording** of the talk.

### Formalizing invisible mathematics

- 13 February 2023
- Talks

I am at the Machine assisted proofs workshop at the UCLA Institute for Pure and Applied Mathematics, where I am about to give a talk on “Formalizing invisible mathematics”.

Here are the slides with speaker notes and the video recording of the talk.

→ continue reading### Exploring strange new worlds of mathematics

- 10 February 2023
- Talks, Constructive math

On February 10, 2023, I gave my Levi L. Conant Lectur Series talk “Exploring strange new worlds of mathematics”, at the math department of Worcester Polytechnic Institute. Here are the slides with speaker notes and the video recording of the talk.

→ continue reading### Happy birthday, Dana!

- 11 October 2022
- News

Today Dana Scott is celebrating the 90th birthday today. **Happy birthday, Dana!** I am forever grateful for your kindness and the knowledge that I received from you. I hope to pass at least a part of it onto my students.

On the occasion Steve Awodey assembled selected works by Dana Scott at `CMU-HoTT/scott`

repository. It is an amazing collection of papers that had deep impact on logic, set theory, computation, and programming languages. I hope in the future we can extend it and possibly present it in better format.

As a special treat, I recount here the story the invention of the famous $D_\infty$ model of the untyped $\lambda$-calculus. I heard it first when I was Dana's student. In 2008 I asked Dana to recount it in the form of a short interview.

→ continue reading (1 comment)### One syntax to rule them all

- 20 May 2022
- Talks

I am at the Syntax and Semantics of Type Theory workshop in Stockholm, a kickoff meeting for WG6 of the EuroProofNet COST network, where I am giving a talk “One syntax to rule them all” based on joint work with Danel Ahman.

→ continue reading### Two new doctors!

- 12 January 2022
- News

Within a month two of my students defended their theses: Dr. Anja Petković Komel just before Christmas, and Dr. Philipp Haselwarter just yesterday. I am very proud of them. Congratulations!

→ continue reading### Is every projective setoid isomorphic to a type?

- 12 January 2022
- Constructive math, Type theory, Formalization

Jacques Carette asked on Twitter for a refence to the fact that countable choice holds in setoids. I then spent a day formalizing facts about the axiom of choice in setoids in Agda. I noticed something interesting that is worth blogging about.

→ continue reading (4 comments)