Skip to content

Reduce #1

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 20 commits into
base: main
Choose a base branch
from
Open

Reduce #1

Show file tree
Hide file tree
Changes from 12 commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
4f3045d
reduce combinator paper
cristianoc Nov 27, 2025
2bfd40c
Formalize reduce semantics and incremental correctness
cristianoc Nov 27, 2025
90da7fc
Clarify distributive aggregates and correctness semantics
cristianoc Nov 27, 2025
6cc4532
Improve exposition of partial reducers and algebraic aggregates
cristianoc Nov 27, 2025
a89264d
aggregates and more examples
cristianoc Nov 27, 2025
a72cc21
Add graph reachability example, e2e test, and clarify paper assumptions
cristianoc Nov 27, 2025
c04df9b
Revert "Add graph reachability example, e2e test, and clarify paper a…
cristianoc Nov 28, 2025
32f7eb1
remove dce example
cristianoc Nov 28, 2025
6755192
fix
cristianoc Nov 28, 2025
a20ddbb
Strengthen abstract/intro with key differentiators from related work
cristianoc Nov 28, 2025
2ee6318
Refine reduce semantics paper: aggregate classes, related work
cristianoc Nov 28, 2025
765f6eb
Refine reduce semantics paper: mini-examples, correctness proof, and …
cristianoc Nov 28, 2025
9478ed5
Remove unnecessary lemma and clarify soundness proof.
cristianoc Nov 28, 2025
4dd50f1
lemma proof layout
cristianoc Nov 28, 2025
3605830
example that illustrates the new lemma
cristianoc Nov 28, 2025
5e53e49
feat: add Lean formalisation of reduce correctness
cristianoc Nov 28, 2025
f1e0b2b
chore: rename Lean project to lean-formalisation
cristianoc Nov 28, 2025
66f91b7
refactor: move Reduce formalisation to top-level module
cristianoc Nov 28, 2025
0146c4d
revise positioning and related work
cristianoc Nov 29, 2025
9372045
tweak related work
cristianoc Nov 29, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,3 +7,5 @@ lib/
*.cmj
*.cmi
*.rei
reduce.aux
reduce.log
Binary file added reduce.pdf
View file
Open in desktop
Binary file not shown.
Loading