progress
A well-typed term is either a value or it can take a step. With preservation, this is type soundness.
Research
A mechanized calculus under the language
LaCaDiLE, the Lambda Calculus for Differentiable Linear Effects, is a Lean 4 mechanization of the core calculus behind Chelis. It models a tensor language with algebraic effects, linear types, and named-dimension indexing.
The mechanization
The development states the metatheory as named Lean theorems. The list below keeps the claims at the theorem boundary: type soundness pieces, dimension safety, effect correctness, linearity soundness, and first-order AD correctness over an abstract primitive AD specification.
preservation
A step from a well-typed term lands in a well-typed term, with the type preserved across evaluation.
dimension_safety
A well-typed term raises no primitive shape mismatch at runtime. Named-dimension agreement checked at compile time holds during execution.
effect_correctness
A well-typed term with an empty effect row never gets stuck performing an effect operation.
linearity_soundness
A step from a well-formed store preserves store well-formedness, so linear resources are not duplicated or dropped incorrectly.
ad_correctness
For the supported first-order fragment, automatic differentiation produces the correct adjoint, mechanized over an abstract primitive AD specification.
Scope is stated precisely in the development. The ad_correctness theorem covers a supported first-order fragment over an abstract primitive AD specification. Higher-order and closure AD are later proof targets, not current theorem claims.