Towards being positively negative about dependent types

Tools

de Muijnck-Hughes, Jan (2025) Towards being positively negative about dependent types. In: 31st Conference on Types for Proofs and Programs, 2025-06-09 - 2025-06-13, University of Strathclyde.

[thumbnail of de-Muijnck-Hughes-TYPES-2025-Towards-being-positively-negative-about-dependent-types]
Preview
 Text. Filename: de-Muijnck-Hughes-TYPES-2025-Towards-being-positively-negative-about-dependent-types.pdf
Preprint
License: Strathprints license 1.0
Download (813kB)| Preview

Abstract

In this talk, I will report work-in-progress that explores what it means to be positively negative when programming with dependent types. I will examine the use of constructive negation to reframe the reporting of decidable procedures and my journey in constructing a library of pure positivity, complete with my journey’s highs and lows. My library demonstrates reasoning about natural numbers, lists, pairs, and strings. I will also examine how being so positive in one's negativity, can reshape how we approach dependently typed programming to better report our program's negativity a bit more positively.

ORCID iDs

de Muijnck-Hughes, Jan ORCID logoORCID: https://orcid.org/0000-0003-2185-8543;
CORE (COnnecting REpositories)