Dependent Types¶

Papers on dependent types from POPL, PLDI, OOPSLA, ECOOP, and ICFP.

2026¶

Local Contextual Type Inference — POPL 2026
Type inference algorithm supporting dependent types via contextual propagation.

2-Functoriality of Initial Semantics — ICFP 2025
Category-theoretic foundations for languages with dependent binding.
Dependent Object Types with Intersection Types — ECOOP 2025
Path-dependent types combined with intersection types in DOT.
Frex: Dependently Typed Algebraic Simplification — ICFP 2025
Free extensions of algebraic structures for certified simplification in Idris.
Linear Types with Dynamic Multiplicities in Dependent Type Theory — ICFP 2025
Dependent linear types with runtime-valued multiplicities, subsuming graded type theories.
McTT: A Verified Kernel for a Proof Assistant — ICFP 2025
Verified Coq-mechanized kernel for Martin-Löf type theory.
Normalization by Evaluation for Non-cumulativity — ICFP 2025
NbE algorithm for type theories with non-cumulative universes.
Type Theory in Type Theory using a Strictified Syntax — ICFP 2025
Internal formalization of type theory using strictified setoid-based syntax.
Type Universes as Kripke Worlds — ICFP 2025
Denotational model interpreting type universes as Kripke worlds.
Verified Compilation of a Dependently Typed Language — PLDI 2025
Coq-verified compiler for a dependent type theory core.