progress
Progress.lean
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
Preservation.lean
A step from a well-typed term lands in a well-typed term, with the type preserved across evaluation.
dimension_safety
DimSafety.lean
A well-typed term raises no primitive shape mismatch at runtime. Named-dimension agreement checked at compile time holds during execution.
effect_correctness
EffectCorrectness.lean
A well-typed term with an empty effect row never gets stuck performing an effect operation.
linearity_soundness
LinearitySoundness.lean
A step from a well-formed store preserves store well-formedness, so linear resources are not duplicated or dropped incorrectly.
ad_correctness
ADCorrectness.lean
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.
Compiler validation
Hull is a reference implementation of the type checker and evaluator, written in Chelis and run alongside the production compiler on generated well-typed programs. Where the two disagree, a spec-implementation bug surfaces. This closes a gap formal work often leaves open: the compiler that implements a proved language can drift from what the proof certifies. LaCaDiLE is the formal specification; Hull is the empirical cross-check that the shipped compiler still matches it.
The proof dispatcher
Specifications enter Chelis as typed program properties. A dispatcher routes each property to the strongest available discharge, cascading through the tiers until one produces a verdict.
- type-level dimension, effect, and linearity properties discharged by the type system at compile time
- SMT (cvc5) algebraic and polynomial properties discharged over the reals by cvc5
- certified-envelope transcendental-bearing goals where each transcendental sub-term (erf, exp, log, sqrt) is replaced by a fresh variable bounded by a certified polynomial envelope, then the residual is discharged by SMT
- bound propagation (beacon) output-range properties verified by propagating interval and zonotope bounds through the compiled DAG, with optional Arb-backed enclosures for sound certification
- randomized validation goals with no formal proof route, covered by seeded reproducible sampling
The first four routes produce proof verdicts over real arithmetic. They make no floating-point roundoff soundness claim: the proof holds over the mathematical reals, and the gap between reals and machine floats is disclosed, not hidden. The fifth route produces a statistical validation verdict with a sample count and seed.
Every result carries provenance: the tier that discharged it, the qualifier set (exact, certified-envelope, sound over-approximation, or fuzz), and the chain back to the originating specification.
Requirements as properties
c-earchin translates structured English requirements, written in EARS notation, into executable Chelis properties bound to the functions they constrain. It handles the EARS patterns (ubiquitous, event, state, unwanted, and optional) and preserves provenance from each requirement line through to the property and its proof artifact. The chain runs from how a specification is written to how it is checked against the implementation.