Towards modular composition of inductive types using Lean meta-programming. ~ Ramy Shahin. msp.cis.strath.ac.uk/types2025/ab... #ITP #LeanProver

Mechanized safety of Jolteon consensus in Agda. ~ Orestis Melkonian, Mauro Jaskelioff, and James Chapman. msp.cis.strath.ac.uk/types2025/ab... #ITP #Agda

…oh, and if you’re here at #types2025 and I haven’t yet introduced myself to you and you’d like to say hi, please do. I’m here to get to know folks.

@joey I don't think so by recent results of @aws, see https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper40.pdf (and the slides and video linked on the TYPES 2025 website).

Geometric reasoning in Lean: from algebraic structures to presheaves. ~ Kenji Maillard, Yiming Xu. msp.cis.strath.ac.uk/types2025/ab... #ITP #LeanProver #Math

HoTTLean: Formalizing the meta-theory of HoTT in Lean. ~ Joseph Hua et als. msp.cis.strath.ac.uk/types2025/ab... #ITP #LeanProver #HoTT

Efficient program extraction in elementary number theory using the proof assistant Minlog. ~ Franziskus Wiesnet. msp.cis.strath.ac.uk/types2025/ab... #ITP #Minlog #Haskell #FunctionalProgramming #Math

Lean4Lean: Mechanizing the metatheory of Lean. ~ Mario Carneiro. msp.cis.strath.ac.uk/types2025/ab... #ITP #LeanProver

Verifying Z3 RUP proofs with the interactive theorem provers Coq/Rocq and Agda. ~ Harry Bryant et als. msp.cis.strath.ac.uk/types2025/ab... #ITP #Coq #Rocq #Agda

hcommons.social:

The recordings from #TYPES2025 are beginning to appear on @mspstrath’s youtube channel. There is a lot of good stuff there already, and I plan to re-watch some talks I enjoyed in the days ahead.Here is the recording of my talk on some of the connections between type theory...

hcommons.social:

…oh, and if you’re here at #types2025 and I haven’t yet introduced myself to you and you’d like to say hi, please do. I’m here to get to know folks.

https://hcommons.social/@consequently/114658662807738778

Löb’s theorem and provability predicates in Rocq. ~ Janis Bailitis1, Dominik Kirst, Yannick Forster. msp.cis.strath.ac.uk/types2025/ab... #ITP #Rocq #Logic #Math

The abstracts for TYPES 2025 are now available at
https://msp.cis.strath.ac.uk/types2025/accepted.html 🎉

I'm involved in two abstracts:

(1) "Representing type theories in two-level type theory" with @Nicolai_Kraus (https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper42.pdf);

(2) […]

A Coq formalization of Lagois connections for secure information flow. ~ Casper Stahl et als. msp.cis.strath.ac.uk/types2025/ab... #ITP #Coq #Rocq

The recordings from #types2025 are beginning to appear on @mspstrath’s youtube channel. There is a lot of good stuff there already, and I plan to re-watch some talks I enjoyed in the days ahead.

Here is the recording of my talk on some of the connections between type theory and issues in […]

TYPES talk done! Time to enjoy the rest of the conference 😄 I talked about injective types in univalent mathematics which is joint work with @MartinEscardo. You can find my slides here https://tdejong.com/talks/TYPES-2025.pdf.

#types2025 #typetheory #hott

Wishing everyone a happy TYPES conference in Glasgow this week.

msp.cis.strath.ac.uk/types2025/

I see the #CallForContributions has gone out for #types #types2025 (International Conference on Types for Proofs and Programs) to be held in Glasgow in June 2025. TYPES "is a forum to present new and ongoing work in all aspects of type theory and its applications, especially in formalised and […]