Towards being positively negative about dependent types

Jan de Muijnck-Hughes

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.

Original language	English
Number of pages	3
Publication status	Published - 13 Jun 2025
Event	31st Conference on Types for Proofs and Programs - University of Strathclyde, Glasgow, United Kingdom Duration: 9 Jun 2025 → 13 Jun 2025 Conference number: 31 https://msp.cis.strath.ac.uk/types2025/ https://msp.cis.strath.ac.uk/types2025

Conference

Conference	31st Conference on Types for Proofs and Programs
Abbreviated title	TYPES 2025
Country/Territory	United Kingdom
City	Glasgow
Period	9/06/25 → 13/06/25
Internet address	https://msp.cis.strath.ac.uk/types2025/ https://msp.cis.strath.ac.uk/types2025

Keywords

Idris
Idris2
dependent types
type theory
verification techniques

Access to Document

de-Muijnck-Hughes-TYPES-2025-Towards-being-positively-negative-about-dependent-typesSubmitted manuscript, 795 KBLicence: Strath_1

Cite this

@conference{bb04d6290bfa46ee9d650733d8d7957a,

title = "Towards being positively negative about dependent types",

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{\textquoteright}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.",

keywords = "Idris, Idris2, dependent types, type theory, verification techniques",

author = "\{de Muijnck-Hughes\}, Jan",

year = "2025",

month = jun,

day = "13",

language = "English",

note = "31st Conference on Types for Proofs and Programs, TYPES 2025 ; Conference date: 09-06-2025 Through 13-06-2025",

url = "https://msp.cis.strath.ac.uk/types2025/, https://msp.cis.strath.ac.uk/types2025",

}

TY - CONF

T1 - Towards being positively negative about dependent types

AU - de Muijnck-Hughes, Jan

N1 - Conference code: 31

PY - 2025/6/13

Y1 - 2025/6/13

N2 - 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.

AB - 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.

KW - Idris

KW - Idris2

KW - dependent types

KW - type theory

KW - verification techniques

UR - https://msp.cis.strath.ac.uk/types2025/

M3 - Abstract

T2 - 31st Conference on Types for Proofs and Programs

Y2 - 9 June 2025 through 13 June 2025

ER -

Towards being positively negative about dependent types

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

31st Conference on Types for Proofs and Programs