Denotational semantics for Laurel IR with concrete evaluator and transform preservation tests#631

Open

olivier-aws wants to merge 15 commits intomainfrom

feat/laurel-denotational-semantics

Commits on Mar 20, 2026

feat(laurel): Add denotational interpreter, semantic helpers, and comprehensive test suite
olivier-aws
committed
fix(laurel): Make denotational semantics exhaustive over all Laurel constructs
olivier-aws
committed
fix(laurel): Address review feedback for Make denotational semantics exhaustive over all Laurel constructs
olivier-aws
committed
fix(laurel): Fix Variables.lean Test 3 block expression in argument position
olivier-aws
committed
chore(test): Remove applyLift parameter from parseLaurel
olivier-aws
committed
fix(laurel): Remove unused simp warnings in LaurelDenoteMono.lean
olivier-aws
committed
feat(test): Add transform preservation tests for Laurel ConcreteEval
olivier-aws
committed
fix(test): Address review feedback for transform preservation tests
olivier-aws
committed
Use lowerLaurelToLaurel in LaurelToCore
olivier-aws
committed
docs(laurel): Move denotational semantics design doc next to implementation
olivier-aws
committed
Add TODO
olivier-aws
committed
fix(laurel): Fix liftExpressionAssignments to preserve evaluation order
olivier-aws
committed
Delete docs/reviews/review-liftimperativeexpressions-diff.md
olivier-aws
authored
Revert unwanted changes
olivier-aws
committed

Commits on Mar 23, 2026

Merge branch 'main' into feat/laurel-denotational-semantics
olivier-aws
authored