search

cue-lang / cue

The home of the CUE language! Validate and define text-based and dynamic configuration
https://cuelang.org
Apache License 2.0
5.02k stars 286 forks source link

Denotational Semantics for CUE #2036

Open myitcv opened 1 year ago

myitcv commented 1 year ago

This is a tracking issue for all things related to denotational semantics and CUE.

More details to follow.

mvdan commented 4 months ago

What was the purpose of this issue? It contains no context and hasn't been updated at all since October 2022. cc @4ad

4ad commented 4 months ago

Currently we do not have a formal semantics for the CUE language. Ideally we would have both an operational and a denotational semantics for CUE with proofs of soundness and adequacy mechanized in some theorem prover.

This issue is an umbrella issue for the denotational semantics work.

The work has been low priority, hence the low (zero) activity in this issue, bu I have some partial semantics of CUE based on topology and Kripke semantics, but they are not mechanized yet. We are planning to pick up the work on this soon though.