MMY MMY (Aug 27 2022 at 11:39): MMY MMY (Aug 27 2022 at 11:39):Hello,
I am very new to Coq.
As part of a project, I need to create denotational semantics and test it with Coq.
I'm trying to transform a piece of code into Coq but I don't know how!
Below is the part of the sematics and my test in Coq:
Definition assignment (var:Exp)( e:Exp) (rhoF :Envf )(rho:Env )(s:State)(Ks :Cs): mSStm :=
let (K0e : Ce) := (v0 , s0) => Ks((rho var) -> v0)
in let (v1,s1) := mExp e rhoF rho s K0e
in s1 .
Paolo Giarrusso (Aug 27 2022 at 13:25):For prospective answerers — see cross-post in https://coq.discourse.group/t/coq-and-denotational-semantics/1771.
(Cross-posting like this isn't encouraged, FWIW).
Paolo Giarrusso (Aug 27 2022 at 13:47):I'm sorry I can't help myself, but I'm not sure what else you've written, how much you know etc. Googling for "denotational semantics in Coq" found https://jhc.sjtu.edu.cn/public/courses/CS263/ which has some notes on a simple denotational semantics.
Alexander Gryzlov (Aug 27 2022 at 13:55):@Jonathan Sterling has the https://github.com/jonsterling/coq-domains library which might help in formalizing denotational stuff (DCPOs etc).
Alexander Gryzlov (Aug 27 2022 at 14:02):Also, there's a short module on den. sem. in this course: https://github.com/xavierleroy/cdf-mech-sem
Karl Palmskog (Aug 27 2022 at 16:05):There might be code on denotational semantics here: https://github.com/coq-community/semantics
MMY MMY (Aug 27 2022 at 17:35):Thanks a lot for your answers.
MMY MMY (Aug 27 2022 at 18:22):I have seen the majority of the references.
I think that's far from what I'm doing.
How can I translate:
K0e of type Ce equal to the torque (v0 , s0).
Paolo Giarrusso (Aug 27 2022 at 19:29):There does not seem to be enough context to answer the question well.
Last updated: Oct 13 2024 at 01:02 UTC