Skip to content

Commit

Permalink
Fixed README formatting
Browse files Browse the repository at this point in the history
  • Loading branch information
Aqissiaq authored Jun 29, 2023
1 parent cd83285 commit 4d2136d
Showing 1 changed file with 9 additions and 9 deletions.
18 changes: 9 additions & 9 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@ Coq mechanization of "Denotational Semantics for Symbolic Execution" for ICTAC23

## Contents
### Main results
- [BigStep](./BigStep.v) covers section 2-3, culminating in Theorem 1: `concrete_symbolic_correspondence`
- [SmallStep](./SmallStep.v) defines and describes the small-step trace semantics of section 4, and
- [Correspondence](./Correspondence.v) proves Theorem 2: `big_small_correspondence`
- [Direct](./Direct.v) proves Proposition 1 (`trace_if_direct` and `direct_if_trace`) and its corollaries `correctness` and `completeness`.
- [BigStep](./BigStep.v) covers section 2-3, culminating in Theorem 1: `concrete_symbolic_correspondence`
- [SmallStep](./SmallStep.v) defines and describes the small-step trace semantics of section 4, and
- [Correspondence](./Correspondence.v) proves Theorem 2: `big_small_correspondence`
- [Direct](./Direct.v) proves Proposition 1 (`trace_if_direct` and `direct_if_trace`) and its corollaries `correctness` and `completeness`.

### Auxilliary materials
- [Expr](./Expr.v) contains the syntax of expressions, and
- [Syntax](./Syntax.v) the syntax of our toy language WHILE
- [Maps](./Maps.v) contains definitions and useful lemmas about total maps used to reason about substitutions and valuations
- [Limits](./Limits.v) contains the use of constructive description to handle non-termination
- Finally, [BigStepExamples](./BigStepExamples.v) contains some examples runs of the big step semantics
- [Expr](./Expr.v) contains the syntax of expressions, and
- [Syntax](./Syntax.v) the syntax of our toy language WHILE
- [Maps](./Maps.v) contains definitions and useful lemmas about total maps used to reason about substitutions and valuations
- [Limits](./Limits.v) contains the use of constructive description to handle non-termination
- Finally, [BigStepExamples](./BigStepExamples.v) contains some examples runs of the big step semantics

## Build
The included Makefile (created for Coq 8.16.1) should allow just
Expand Down

0 comments on commit 4d2136d

Please sign in to comment.