frap
frap copied to clipboard
achlipala
Formal Reasoning About Programs
I am trying to use the Coq files of the textbook, and ran into an issue when I ran `make lib`. ### Steps to reproduce: 1. Clone repository 2. Run...
I was wondering if there were any plans on releasing it there. Thanks!
Something of a feature request, but perhaps it might be nice to have a "Further Reading" section at the end of each chapter with links to some relevant papers/readings? I've...
I was reading AbstractInterpretation.v's definitions of [absint_sound](https://github.com/achlipala/frap/blob/51a7fae33e0056581cb3ab7e7595090cad97878a/AbstractInterpretation.v#L44) and [absint_complete](https://github.com/achlipala/frap/blob/51a7fae33e0056581cb3ab7e7595090cad97878a/AbstractInterpretation.v#L81), and found them quite challenging to read because of the verbosity. I thought I'd try rewriting it a bit to more...
Disclaimer: I am a coq noob Edit: resolved by using a global opam switch As stated in the [.tex sources](https://github.com/achlipala/frap/blob/master/frap_book.tex#L87) I used coq `8.16.0` (I also tried with `8.15.0` to...
``` The Coq Proof Assistant, version 8.17.0 compiled with OCaml 4.14.0 macOS Big Sur Version 11.5.2 ``` At first, I was getting the following error ``` The default value for...
Hi, I'm trying to build the project as stated in the README, but `make all` fails with make -f Makefile.coq make[1]: Entering directory '/home/bedef/Projects/coq/frap' /bin/sh: line 1: /snap/coq-prover/34/coq-platform/bin//coqc: No such...
I spent a while looking at the proof of `withInterference_parallel` (in the ModelChecking file) without being able to understand it, so I tried to write a simpler proof. Obviously my...
