Decorated proofs for computational effects: States
Jean-Guillaume Dumas (LJK, Universit\'e de Grenoble, France),, Dominique Duval (LJK, Universit\'e de Grenoble, France), Laurent Fousse (LJK,, Universit\'e de Grenoble, France), Jean-Claude Reynaud (LJK, Universit\'e de, Grenoble, France)
TL;DR
This paper demonstrates that equational proofs in imperative languages can implicitly represent state, aligning the proof methodology with the language's syntax which does not explicitly mention state.
Contribution
It introduces a method to hide state within equational proofs, bridging the gap between syntax and semantics of imperative languages.
Findings
Equational proofs can implicitly encode state effects.
The approach aligns proof techniques with language syntax.
Provides a new perspective on reasoning about state in imperative languages.
Abstract
The syntax of an imperative language does not mention explicitly the state, while its denotational semantics has to mention it. In this paper we show that the equational proofs about an imperative language may hide the state, in the same way as the syntax does.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · DNA and Biological Computing · Logic, Reasoning, and Knowledge