index
:
rego-proofs.git
master
merge-parsing-stages
Lean proofs for my Master's thesis
Jakob L. Kreuze
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2023-12-22
Prove remaining `sorry' statements
HEAD
master
Jakob L. Kreuze
2023-12-22
Finish proving `pr'
Jakob L. Kreuze
2023-12-22
Prove ta_external_grades_not_applicable
Jakob L. Kreuze
2023-12-21
Add README
Jakob L. Kreuze
2023-12-21
Update lemmas
Jakob L. Kreuze
2023-12-21
s/simp/rfl/ where necessary
Jakob L. Kreuze
2023-12-21
LawfulBEq proofs
Jakob L. Kreuze
2023-12-21
Get rid of old compiler code
Jakob L. Kreuze
2023-12-21
Check-in remaining files
Jakob L. Kreuze
2023-12-21
Check-in 2023-12-21
Jakob L. Kreuze
2023-12-21
Check-in 2023-12-15
Jakob L. Kreuze
2023-12-21
Check-in 2023-12-11
Jakob L. Kreuze
2023-12-21
Check-in 2023-12-07
Jakob L. Kreuze
2023-12-21
Check-in 2023-12-06
Jakob L. Kreuze
2023-12-19
Fix match evaluation
Jakob L. Kreuze
2023-12-19
Initial check-in of XACML implementation in Rego
Jakob L. Kreuze
2023-12-05
Support compilation of multiple files
Jakob L. Kreuze
2023-12-05
Proper executable for XACML compiler
Jakob L. Kreuze
2023-11-16
Use fold_and where necessary
Jakob L. Kreuze
2023-11-16
Fix compilation of function arguments
Jakob L. Kreuze
2023-11-15
Have evaluate_policy* take the results of its children as a parameter
Jakob L. Kreuze
2023-11-15
Add semantics for obligation/advice expressions
Jakob L. Kreuze
2023-11-15
Clearer translation of XACML to Rego values
Jakob L. Kreuze
2023-11-15
Initial encoding of XACML semantics in Rego
Jakob L. Kreuze
2023-11-10
Compile error condition
Jakob L. Kreuze
2023-11-10
Handle nested parameters
Jakob L. Kreuze
2023-11-09
Handle else keyword
Jakob L. Kreuze
2023-11-07
Basic expression simplification
Jakob L. Kreuze
2023-11-07
Fix parsing issue for set rules
Jakob L. Kreuze
2023-11-07
Compile imports (not really)
Jakob L. Kreuze
2023-11-07
Re-instate assignment order assertion
Jakob L. Kreuze
2023-11-07
Handle existential quantification over objects
Jakob L. Kreuze
2023-11-03
Checkpoint
Jakob L. Kreuze
2023-11-03
More reliable handling of rules with formal parameters
Jakob L. Kreuze
2023-11-03
Ensure identifiers produced by gensym are legal Lean variable names
Jakob L. Kreuze
2023-11-02
Add support for Negate rules
Jakob L. Kreuze
2023-11-02
Parse Negate properly
Jakob L. Kreuze
2023-11-02
Compile functions
Jakob L. Kreuze
2023-11-02
Minor refactoring
Jakob L. Kreuze
2023-11-01
Initial attempt at compiling rules with sets/objects as headsa
Jakob L. Kreuze
2023-11-01
Fix assignment rule parsing
Jakob L. Kreuze
2023-11-01
Compile default rules
Jakob L. Kreuze
2023-11-01
Compile references to inductively-defined variables
Jakob L. Kreuze
2023-11-01
Replace complete with more detailed description of variable usage
Jakob L. Kreuze
2023-10-31
Add support for nested definitions
Jakob L. Kreuze
2023-10-31
Use gensym for generated identifiers
Jakob L. Kreuze
2023-10-31
Error on variables used before assignment
Jakob L. Kreuze
2023-10-31
Assigned field for variable records
Jakob L. Kreuze
2023-10-31
More detailed variable usage analysis
Jakob L. Kreuze
2023-10-31
No longer need to pass up local definitions
Jakob L. Kreuze
[next]
© 2015 - 2026 Jakob L. Kreuze