Timeline for How do I define a function in Coq with if...then..else behavior?
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 11, 2023 at 12:59 | comment | added | Pietro Braione | Thank you for the references, I will definitely check them. | |
| Jan 9, 2023 at 18:45 | comment | added | Andrej Bauer | Related work in this case should not be ignored. A shallow search reveals CoqJVM: An Executable Specification of the Java Virtual Machine using Dependent Types and A Formal Executable Semantics of the JavaCard Platform, at least. | |
| Jan 9, 2023 at 10:47 | comment | added | Pietro Braione | Not really familar, but I am perusing Software Foundations as reference, it helps me a lot, and I shall read it more systematically in the future. To explain better whst I am doing, I am modeling a trimmed down version of the JVM specification, so the Coq model must be not too abstract to stay faithful to the original document. Explaining the motivation is always a tradeoff game between giving a meaningful context and not burdening the explanation or asking other people to do your work, sorry if I was not effective in that regard. | |
| Jan 8, 2023 at 17:32 | comment | added | Andrej Bauer | Are you familiar with Software foundations? It might be a useful source of knowledge for your purposes. | |
| Jan 8, 2023 at 17:30 | comment | added | Andrej Bauer | It's usually better not to provide "fake motivation". If you stated from the beginning that you were doing semantics of an object-oriented language, you could have gotten a much more useful answer. A simple programming language (of whatever kind) can be dealt with quite easily in Coq. | |
| Jan 8, 2023 at 17:03 | comment | added | Pietro Braione | I want to give operational semantics via a step transition relation, then define a symbolic operational semantics, and prove the latter to be equivalent to the former. The actual language is an OO language with multiple classes and methods, so there are many more structural invariants than just having distinct locations for distinct statements. That's why I do not specify programs as maps from locations to statements - every method would have its map and I would still have to specify all these maps do not overlap. So I express all the invariants via a predicate. | |
| Jan 8, 2023 at 14:41 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 236 characters in body
|
| Jan 8, 2023 at 10:32 | history | answered | Andrej Bauer | CC BY-SA 4.0 |