Showing cs.LOShow all
3 papers · 1 filter
cs.LO2026
Ultraconstructive Model Theory via Bounded Adversarial Finite Structures
Mirco A. Mannucci
Ultraconstructive Model Theory (UCMT) replaces idealized satisfaction, at finite compu- tational scale, by bounded adversarial survival. A finite partial structure is tested by an…
cs.LO2026
Resource-Bounded Martin-Löf Type Theory: Compositional Cost Analysis for Dependent Types
Mirco A. Mannucci, Corey Thuro
We extend resource-bounded type theory to Martin-Lof type theory (MLTT) with dependent types, enabling size-indexed cost bounds for programs over inductive families. We introduce a…
cs.LO2025
Resource-Bounded Type Theory: Compositional Cost Analysis via Graded Modalities
Mirco A. Mannucci, Corey Thuro
We present a compositional framework for certifying resource bounds in typed programs. Terms are typed with synthesized bounds drawn from an abstract resource lattice, enabling uni…