|
|
- Automated Proving Correctness of Transformations for the Program Calculus Lneed
-
The calculus LR is an extended call-by-need lambda calculus with letrec, data constructors, case-expressions, and the seq-operator.
The calculus and program transformations are modeled in the LRSX Tool by the following input files:
Some exemplary calls of the LRSX Tool are:
- compute forking and answer diagrams and write them into file output with full proofs:
lrsx join proofs bound=12 LR-FORK.inp > output_proofs
- compute forking and answer diagrams and write them into file output in long format:
lrsx join proofs bound=12 LR-FORK.inp > output.long
- convert diagrams from long into short format, where the input is in file output.long and the output is written into output_short:
lrsx convert long short output.long > output_short
- compute commuting and answer diagrams and write them into file output in long format:
lrsx join proofs bound=12 LR-COMMUTE.inp > output.long
- convert the commuting diagrams in file output.long into a TRS:
lrsx convert long trs output.long > output_trs
- perform the induction on diagrams in input.long where atppath contains AProVE and CeTA,
the TRSs are written to outpath, termination proofs are written to proofs:
lrsx induct atp-path=atppath output-to=outpath input.long > proofs
- Output of the LRSX Tool
-
- Contact
-
David Sabel
|