Skip to content

Commit f9ec1c8

Browse files
committed
Update README
1 parent c28d37f commit f9ec1c8

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

README.md

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
# Isabelle proving project - Semantics of functional programming languages
22

3-
In this project I want to start with a simply typed lambda calculus, prove type soundness and then extend it step by step until I am at the [latest version of System F](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs) used in GHC.
3+
![Build](https://github.com/jvanbruegge/isabelle-lambda-calculus/workflows/Build/badge.svg)
44

5-
I am using [ott](https://github.com/ott-lang/ott) to generate Isabelle code for the definitions of the systems
5+
In this project I want to start with a simply typed lambda calculus, prove type soundness and then extend it step by step until I am at the [latest version of System F](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs) used in GHC.
66

77
## Roadmap
88

@@ -14,6 +14,7 @@ I am using [ott](https://github.com/ott-lang/ott) to generate Isabelle code for
1414
- [x] Extend definition
1515
- [x] Prove Progress
1616
- [x] Prove Preservation
17+
- [x] Use the Nominal2 framework to reason about alpha-equated terms
1718
- [ ] Add datatypes and `case` expressions
1819
- [ ] Extend definition
1920
- [ ] Prove Progress

0 commit comments

Comments
 (0)