Riccardo Borsetto

Software / Formalizations

Active projects

s4dot2-cut-elimination

This Cubical Agda development formalizes cut elimination and the finite model property for S4.2. It is the formal artifact accompanying the S4.2 papers.

nuclear

This Cubical Agda project proves conservation theorems for nuclei over substructural entailment relations, taking Full Lambek logic as the base system. It is the formal artifact of the CiE 2026 paper and includes contributions by Thorsten Altenkirch. Rendered Agda HTML.

regcat-normal-form

This Agda development gives a machine-checked canonical normal form theorem for the type theory of regular categories. It contains a complete Tait-style logical-relations proof, and all modules use --safe.

lean-archimedean-portfolio

This Lean 4 and Mathlib project treats the witness-extraction Archimedean property as a typeclass and proves it equivalent to Mathlib’s Archimedean property. It is a companion to the TYPES 2026 abstract.

agdarya

This OCaml project is a fork of Narya, a higher-dimensional observational type theory proof assistant, with Agda-style syntax and layout-sensitive parsing.

Contributions to LorenzoMolena/cubical

My merged pull requests to this experimental Cubical Agda library concern constructive real analysis: Cauchy completion, premetric spaces, univalence of PrSpaces, and a domain-specific language.

cartmell-thesis

A community effort, with Peter LeFanu Lumsdaine and others, to typeset John Cartmell’s PhD thesis, Generalised Algebraic Theories and Contextual Categories, in TeX.

Archived or superseded