Burak Ekici

IMP with exceptions over decorated logic

Keywords: Computational effects, state, exceptions, program equivalence proofs, decorated logic, Coq

In this paper, we facilitate the reasoning about impure programming languages, by annotating terms with "decorations" that describe what computational (side) effect evaluation of a term may involve. In a point-free categorical language, called the "decorated logic", we formalize the mutable state and the exception effects first separately, exploiting a nice duality between them, and then combined. The combined decorated logic serves as the target language for the denotational semantics of the IMP+Exc imperative programming language, and allows us to prove equivalences between programs written in IMP+Exc. The combined logic is encoded in Coq, and this encoding is used to certify some program equivalence proofs.

Introduction

In programming languages theory, a program is said to have computational effects if, besides a return value, it has observable interactions with the outside world. For instance, using/modifying the program state, raising/recovering exceptions, reading/writing data from/to some file, etc. In order to formally reason about behaviors of a program with computational effects, one has to take into account these interactions. One difficulty in such a reasoning is the mismatch between the syntax of operations with effects and their interpretation. Typically, an operation in an effectful language with arguments in X that returns a value in Y is not interpreted as a function from X to Y , due to the effects, unless the operation is pure.

The best known algebraic approach to formalize computational effects was initiated by [START_REF] Moggi | Notions of computation and monads[END_REF] in his seminal paper. He showed that the effectful operations of an impure language can be interpreted as arrows of a Kleisli category for an appropriate monad (T, η, µ) over a base category C with finite products. For instance, in Moggi's computational metalanguage, an operation in an impure language with arguments in X that returns a value in Y is now interpreted as an arrow from X to T Y in C where X is the object of values of type X and T Y is the object of computations that return values of type Y . The use of monads to formalize effects (such as state, exceptions, input/output and non-deterministic choice) was popularized by [START_REF] Wadler | The essence of functional programming[END_REF], and implemented in the programming languages Haskell and F . Using monad transformers, as in [START_REF] Jaskelioff | Modular monad transformers[END_REF], it is usually possible to "combine" different effects formalized by monads. Moggi's computational metalanguage was extended into the basic effect calculus with a notion of computation type by [START_REF] Filinski | Controlling Effects[END_REF] in his effect PCF and by [START_REF] Levy | Call-by-push-value: A subsuming paradigm[END_REF] in his call-by-push-value (CBPV). [START_REF] Egger | The enriched effect calculus: syntax and semantics[END_REF] defined their effect calculus, named extended effect calculus as a canonical calculus incorporating the ideas of Moggi, Filinski and Levy. Following Moggi, they included a type constructor for computations. Following Filinski and Levy, they classified types into value types and computation types.

Being dual to monads, comonads have been used to formalize context-dependent computations. Intuitively, an effect which observes features may arise from a comonad, while an effect which constructs features may arise from a monad [START_REF] Jacobs | An introduction to (co)algebras and (co)induction[END_REF]). [START_REF] Uustalu | Comonadic notions of computation[END_REF] have structured stream computations, [START_REF] Orchard | Ypnos: Declarative, parallel structured grid programming[END_REF] array computations and [START_REF] Tzevelekos | Nominal game semantics[END_REF] game semantics via the use of comonads. Petricek et al. proposed a unified calculus for tracking context dependence in functional languages together with a categorical semantics based on indexed comonads. In [START_REF] Orchard | Should i use a monad or a comonad?[END_REF]), there is a quite nice discussion on how to choose between a monad or comonad when either can be used to capture a particular notion of computation. Also, [START_REF] Brookes | Monads and Comonads in Intensional Semantics[END_REF] discussed that a computation may be interpreted by distributive laws of a comonad over a monad when it is seen as a composition of context-dependence and effectfulness. This approach has been applied to clocked causal data-flow computation, combining causal data-flow and exceptions by [START_REF] Uustalu | The essence of dataflow programming[END_REF].

Moggi's approach, using monads in effect modeling, has been extended to Lawvere theories which first appeared in [START_REF] Lawvere | Functorial Semantic of Algebraic Theories (Available with commentary as TAC Reprint 5[END_REF]'s PhD dissertation. Then, [START_REF] Linton | Some aspects of equational theories[END_REF][START_REF] Linton | Relative functorial semantics: adjointness results[END_REF] first showed that every Lawvere theory induces a monad on the category of sets, and then on any category satisfying some condition called the "local representability". Therefore, Moggi's seminal idea, formalizing computational effects by monads, made it possible for monadic effects to be formalized through Lawvere theories. To this extend, [START_REF] Plotkin | Notions of computation determine monads[END_REF] have shown that effects such as the global and the local state could be formalized by signatures of effectful terms and an equational theory explaining the interactions between them. [START_REF] Melliès | Segal condition meets computational effects[END_REF] has refined this equational theory showing that some of the equations modeling the mutable global state can be omitted. [START_REF] Hyland | Combining effects: Sum and tensor[END_REF][START_REF] Hyland | Combining algebraic effects with continuations[END_REF] studied the combination of computational effects in terms of Lawvere theories. Plotkin andPretnar (2009, 2013) extended Moggi's classification of terms (values and computations) with a third level called handlers for the computational effects that can be represented by an algebraic theory (algebraic effects). Initially, they introduce an handler for the exception handling, and then account for its generalization to the other handlers to cope with other algebraic effects such as stream redirection, explicit non-determinism, CCS, parameter passing, timeout and rollback (Plotkin and Pretnar, 2013, §3). For each algebraic effect, handling constructs are used to apply handlers to effectful computations where effectful computations can be interpreted as algebraic operations while handling constructs as homomorphisms from free algebras. This use of handling constructs is inspired from [START_REF] Benton | Exceptional syntax[END_REF]'s work where a single construct specialized to handle exceptions is introduced. Moreover, [START_REF] Jacobs | A formalisation of java's exception mechanism[END_REF] formalized the exception effect from the dual, namely co-algebraic, viewpoint. Exception handling is also used to build a Hoare logic for exceptions by [START_REF] Schröder | Generic exception handling and the Java monad[END_REF].

There is an older formal way of modeling computational effects called the effect systems by [START_REF] Lucassen | Polymorphic effect systems[END_REF]. They presented an approach to programming languages for parallel computers. The key idea was to use an effect system to discover expression scheduling constraints. There, every expression comes with three components: types to represent the kinds of the return values, effects to summarize the observable interactions of expressions and regions to highlight the areas of the memory where expressions may have effects. To this extend, one can simply reason that if two expressions do not have overlapping effects, then they can obviously be scheduled in parallel. The reasoning is done by some inference rules for types and effects based on the second order typed λ -calculus. [START_REF] Domínguez | Diagrammatic logic applied to a parameterisation process[END_REF] proposed yet another paradigm to formalize computational effects by mixing effect systems and algebraic theories, named the decorated logic. The key point of this paradigm is that every term comes with a decoration which exposes its features with respect to a single computational effect or to several ones keeping their interpretations close to syntax in reasoning with effects. In addition, an equational theory highlights the interactions among terms with two sorts of equations: weak equations relate terms with respect only to their results while strong equations relate them with respect both to their results and effects. By and large, decorated logic provides an equational reasoning in between programs written in imperative languages after being used as a target language for a denotational semantics of the studied language.

In a decorated logic, a term has three different decorations: pure, accessor and modifier/catcher. The first two decorations can correspond to Moggi's values and computations, and the third level can be seen as Plotkin and Pretnar's handlers. An handler operates recursively by its nature, and handles also the continuation. However, a catcher does not. It returns the continuation unhandled which should then be handled explicitly. Thus, catchers are non-recursive handlers, so called shallow handlers introduced by [START_REF] Kammar | Handlers in action[END_REF].

On the use of decorated logic

In this paper, we use Duval's decorated logic to formalize computational effects. The advantages of using decorated logic in effect formalization is mainly two-folded: (1) effects of terms are hidden by the decorations, so that it is possible to preserve the syntax of term signatures. Thereafter, the provided equational reasoning would be valid for different algebraic models of the same effect. (2) The equational theory is based on decorated equivalence relations proposing different reasoning capabilities: one on effects and returned results and the other one only on returned results. However, for the time being, it might be inconvenient to use decorated logic to prove more general properties of algorithms. That is to say, we can prove equivalences between programs that admits particular specifications as initializing and describing final values stored in variables. The total correctness of a theory in a decorated logic, that guaranties that the theory is not using too many axioms to become the maximal theory, is based on a syntactic completeness property called relative Hilbert-Post completeness. Section 7.3 details mentioned property, and its application to the specific case that this paper covers.

Organization and contributions

In general terms, in this paper, we extend Moggi's original approach using the classifications of expressions, provided by the Kleisli category of the monad of exception and the comonad of the state thanks to the duality between states and exceptions proven by [START_REF] Dumas | A duality between exceptions and states[END_REF]. The definitions and the results are presented in terms of equational theories so that one does not need to know the details about the monad of exceptions nor the comonad of the state. In more specific terms, this paper designs the decorated logic for the global state and the exception effects, and then combines them to serve as a target language for denotational semantics of imperative programming languages mixing mentioned effects. It is organized as follows: in Section 2, we introduce an imperative programming language that mixes the state and the exception effects by defining its small-step operational semantics. The language we study there is called IMP+Exc which extends the IMP (or while) with a mechanism to raise and handle exceptions. In Section 3, we introduce the decorated logic as a generic framework extending Moggi's monadic equational logic. Then, we formally specialize the decorated logic for the state and the exception effects in Sections 4 and 5, respectively. In Section 6, we combine these logics. Finally, Section 7 details the use of the combined decorated logic as the target language for the IMP+Exc denotational semantics. This provides a rigorous formalism for an equational reasoning between termination-guaranteed IMP+Exc programs. I.e., proving two different looking programs are in fact doing the same job with respect to the state and exception effects. In Section 7.1, we presents three proof examples. Also, we certify such proofs with the Coq Proof Assistant. See the entire Coq implementation here (i) , and the approach of the paper in Figure 1. This paper builds upon several papers by [START_REF] Domínguez | Diagrammatic logic applied to a parameterisation process[END_REF], Dumas et al. (2014a), [START_REF] Dumas | Relative hilbert-post completeness for exceptions[END_REF], Dumas et al. (2014b), [START_REF] Dumas | A duality between exceptions and states[END_REF] and Dumas et al. (2014c) . The novel points presented here can be itemized as follows:

Decorated logic

• a combined decorated logic for the states (Dumas et al. (2014a)) and exceptions (Dumas et al. (2014b)) effects (this paper explains both logics again but for the details please refer to the citations),

• Coq formalization of the combined logic,

• a denotational semantics for the IMP+Exc (IMP with exceptions) over the combined logic,

• Coq formalization of the IMP+Exc denotational semantics,

• some equivalence proofs of programs written in IMP+Exc and their verifications in Coq.

A preliminary version of this paper has been presented in TFP (Trends in Functional Programming) 2015 but did not appear in the final proceedings. Find the mentioned paper here (ii) .

IMP with exceptions

IMP is a standard Turing complete imperative programming language natively providing global variables of integer (Z), Boolean (B) and unit (U) data types, standard integer and Boolean arithmetic enriched with a set of commands that is made of do-nothing, assignment, sequence, conditionals and looping operations. Below, we detail its syntax where n represents a constant integer term while x is an integer global variable. Note also that abbreviations aexp and bexp respectively denote arithmetic and Boolean expressions as well as cmd stands for the commands.

aexp: (i) https://github.com/ekiciburak/impex-on-decorated-logic (ii) ftp://ftp-sop.inria.fr/indes/TFP15/TFP2015_submission_6.pdf Neither arithmetic nor Boolean expressions are allowed to modify the state: they are either pure or read-only. We present, in Figure 3, the big-step semantics for evaluation of arithmetic expressions in IMP where we use a big-step transition function → a : aexp × S → Z. This function computes an integer value out of an input arithmetic expression and the current program state (denoted s) which includes contents of variables at a given time. The symbol op represents the operation symbols (+,or ×) given by the The small-step operational semantics for evaluation of commands are given in Figure 5 where we use a small-step transition function : S × cmd → S × cmd which is interpreted as at the state s, one step execution of the command c changes the state into s and the command c is now in further execution. We need to elucidate that a command c terminates at a state s if s, c * s , SKIP for some state s , where * is the transitive closure of the transition function . Mind also that SKIP is allowed to execute at any state s, and SKIP alone is used to indicate the final step of some command set.

a 1 a 2 ::= n | x | a 1 + a 2 | a 1 -a 2 | a 1 × a 2 bexp: b 1 b 2 ::= true | false | a 1 ? = a 2 | a 1 ? = a 2 | a 1 ? > a 2 | a 1 ? < a 2 | b 1 ∧ b 2 | b 1 ∨ b 2 | ¬b 1 cmd: c 1 c 2 ::= SKIP | x a 1 | c 1 ; c 2 | if b then c 1 else c 2 | while b do c 1 Figure 2: Standard IMP syntax
(aconst) (n, s) → a n (var) (x, s) → a s(x) (op -sym) (a 1 , s) → a n 1 (a 2 , s) → a n 2 (a 1 op a 2 , s) → a n 1 op Z n 2
(true) (true, s) → b true (false) (false, s) → b f alse (op1) (b 1 , s) → b v 1 (b 2 , s) → b v 2 (b 1 opb b 2 , s) → b v 1 opb B v 2 (op2) (b 1 , s) → b v 1 (¬ b 1 , s) → b neg v 1
(sequence) s, c 1 s , c 1 s, (c 1 ; c 2 ) s , (c 1 ; c 2 ) (skip) s, (SKIP; c) s, c (assign) (a, s) → a n s, (x := a) s[x ← n], SKIP (cond 1 ) (b, s) → b true s, (if b then c 1 else c 2 ) s, c 1 (cond 2 ) (b, s) → b f alse s, (if b then c 1 else c 2 ) s, c 2 (while 1 ) (b, s) → b true s, (while b do c) s, (c; while b do c) (while 2 ) (b, s) → b f alse s, (while b do c) s, SKIP

A mechanism to handle exceptions

Extending the IMP language with a mechanism that allows raising exceptions and recovering from them, we enrich the command set with THROW and TRY/CATCH blocks. In addition to the ones in Figure 2, we also consider following commands in Figure 6 Exceptional commands are pure in terms of the state effect: they neither use nor modify the program state. However, they introduce another sort of computational effect: the exception. In prior, we stated that the command SKIP alone indicates the termination of a program. Now, we extend this by saying THROW e is also an end but an abnormal end. Intuitively, if an exceptional value of name e is raised in the TRY block and recovered immediately in the CATCH, the program then resumes with the provided continuation. An exceptional value (of name e) gets propagated if another exceptional value with different name (say, of name f, s.t. e = f) is being recovered in the CATCH.

In Section 7, we define denotational semantics of the IMP+Exc language using the decorated logic (generic framework is given in Section 3) for the state and the exception effects as the target language. We present this logic in Section 6 as a combination of the logics that we introduce in Sections 4 and 5.

3 Decorated Logic (L dec )

The decorated logic, as a generic framework, is an extension to monadic equational logic [START_REF] Moggi | Notions of computation and monads[END_REF], that we briefly discuss in Section 3.1, with the use of decorations on terms and equalities. It provides a rigorous formalism to do equational reasoning between impure programs written in imperative programming languages with side effects after being defined as a target language for their denotational semantics.

Monadic Equational Logic (L meq )

The monadic equational logic (L meq ) is the minimal logic that can be interpreted in a category with objects as types, arrows as terms and equalities as equations. I.e., an object O in the category interprets the type X in the logic, just as the usual Leibniz equality, f = g, interprets the equation f ∼ = g in the logic. The keyword "monadic" has little to do with monads. It rather means that the operations of the logic are unary (or mono-adic). Figure 8 presents the syntax of the logic L meq . There, every term has a source and a Grammar for the monadic equational logic: target type, e.g., f : X → Y. Every equation is formed by terms with the same source and target types, e.g., e : f ∼ = g where f, g : X → Y. This syntax is accompanied by the rules shown in Figure 9.

Types: t ::= X | Y | . . . Terms: f, g ::= id t | a | b | • • • | g • f Equations: eq ::= f ∼ = g
congruence rules The congruence rules say that the relation ' ∼ =' is a congruence meaning that it is an equivalence relation (reflexive, symmetric and transitive) which obeys replacements and substitutions of compatible terms with respect to the composition. The basic categorical rules indicate that there is an identity morphism id X : X → X for each type X, composition is an associative operation, and composing any term f with id is f, up to ∼ =, no matter the composition order.

(refl) f f ∼ = f (sym) f ∼ = g g ∼ = f (trans) f ∼ = g g ∼ = h f ∼ = h (replsubs) f 1 ∼ = f 2 : X → Y g 1 ∼ = g 2 : Y → Z g 1 • f 1 ∼ = g 2 • f 2 categorical rules (id) X id X : X → X (comp) f : X → Y g : Y → Z (g • f) : X → Z (ids) f : X → Y f • id X ∼ = f (idt) f : X → Y id Y • f ∼ = f (assoc) f : X → Y g : Y → Z h : Z → U h • (g • f) ∼ = (h • g) • f

The decorated logic

The decorated logic extends the monadic equational logic with a 3-tier effect system for terms and a 2-tier system for equations made of "up-to-effects" (weak) and "strong" equalities. Figure 10 presents its syntax. Each term has a source and a target type as well as a decoration which describe what computational side effects evaluation of that term may involve, and used as a superscript (0), (1) or (2): a pure term is decorated with (0), an effect constructor with (1) and an effect modifier term comes with the decoration (2). Each equation is formed by two terms with the same source and target as well as a decoration which is denoted either by "∼" (weak) or by "≡" (strong). A weak equality between two terms relates them according only to their results, while a strong equality relates terms according both to their result and the side effect evaluations they involve with respect to the effect in question.

Grammar for the decorated logic: The tpure is a special constructor used to introduce decorated pure terms into the logic L dec . It inputs a non-decorated pure term from a pure type system (i.e., Coq's logic) and drops it in with the decoration (0). For instance, the identity term id is defined using the tpure constructor, for all types X as follows:

Types: t ::= X | Y | . . . Decoration for terms: (d) ::= (0) | (1) | (2) Terms: f, g ::= a (d) | b (d) | • • • | g • f (d) | (tpure • ) (0) Equations: eq ::= f ≡ g | f ∼ g
id (0) X :
X → X := tpure (λ x : X. x : X).

In Figure 11, we present the inference rules associated to the syntax given in Figure 9. Remark 3.1. In all of the figures presenting the rules of some decorated logic, through out the paper, the decorations "d 1 , d 2 , d 3 , . . . " are meant to be in the set {0, 1, 2} unless otherwise stated. For instance, in the rule (wtos) below decorations d 1 and d 2 cannot take the value 2.

hierarchy rules

(0-to-1) f (0) f (1) (1-to-2) f (1) f (2) (stow) f (d 1 ) ≡ g (d 2 ) f (d 1 ) ∼ g (d 2 ) (wtos) f (d 1 ) ∼ g (d 2 ) d 1 , d 2 ∈ {0, 1} f (d 1 ) ≡ g (d 2 ) congruence rules (refl) f (d 1 ) f (d 1 ) ≡ f (d 1 ) (sym) f (d 1 ) ≡ g (d 2 ) g (d 2 ) ≡ f (d 1 ) (trans) f (d 1 ) ≡ g (d 2 ) g (d 2 ) ≡ h (d 3 ) f (d 1 ) ≡ h (d 3 ) (wrefl) f (d 1 ) f (d 1 ) ∼ f (d 1 ) (wsym) f (d 1 ) ∼ g (d 2 ) g (d 2 ) ∼ f (d 1 ) (wtrans) f (d 1 ) ∼ g (d 2 ) g (d 2 ) ∼ h (d 3 ) f (d 1 ) ∼ h (d 3 ) (replsubs) f (d 1 ) 1 ≡ f (d 2 ) 2 : X → Y g (d 3 ) 1 ≡ g (d 4 ) 2 : Y → Z g (d 3 ) 1 • f (d 1 ) 1 ≡ g (d 4 ) 2 • f (d 2 ) 2 categorical rules (comp) f (d 1 ) : X → Y g (d 1 ) : Y → Z (g • f) (d 1 ) : X → Z (assoc) f (d 1 ) : X → Y g (d 2 ) : Y → Z h (d 3 ) : Z → U h (d 3 ) • (g (d 2 ) • f (d 1 ) ) ≡ (h (d 3 ) • g (d 2 ) ) • f (d 1 ) (ids) f (d 1 ) : X → Y f (d 1 ) • id (0) X ≡ f (d 1 ) (idt) f (d 1 ) : X → Y id (0) Y • f (d 1 ) ≡ f (d 1 ) (tcomp) f (p) : Y → Z g (p) : X → Y (tpure f) (0) • (tpure g) (0) ≡ (tpure (f • g)) (0) Figure 11: L dec : rules Lemma 3.2. ∀f (d 1 ) : X → Y, g (d 2 ) : Y → Z, the annotation (g • f) (max(d 1 ,d 2 )) is admissible.
Proof: Trivially follows from case analyses on d 1 and d 2 , and the rules (0-to-1), (1-to-2) and (comp).

Hierarchically, a pure term can be seen as a constructor (0-to-1), and similarly a constructor term can be seen as a modifier on demand (1-to-2).

It is obviously free to convert strong equations into weak ones (stow). However, one has to make sure that the equated terms are not decorated with (2) in order to convert weak equations into strong ones with no further evidence (wtos).

Both strong and weak equalities are defined to be equivalence relations with the assumption that they are reflexive, transitive and symmetric. Strong equations form a congruence relation but weak equations do not: we will see this in detail when we specialize the decorated logic for the global state and the exception effects in Sections 4 and 5, respectively.

The categorical rules present properties of the term composition: the decoration of a composition depends on the decoration of its components, always taking the larger. I.e., ∀ f (0) : X → Y and g (2) : Y → Z, g • f : X → Z takes the decoration (2) (Lemma 3.2). Composition is an associative operation (assoc). The identity term disappears when to compose on the right (ids), and on the left (idt). The rule (tcomp) states that the tpure constructor preserves the composition of pure terms up to the strong equality. Meaning that one can first compose pure terms outside the decorated environment (in any pure type system) and use the tpure constructor to translate them into the L dec , or translate the terms into the L dec first, and then compose them there. Notice that the red colored composition symbol (•), in the rule conclusion, stands for the composition operation for pure terms. The decoration (p) of terms f and g is used just to denote the pure terms outside decorated environment, thus it does not take part in the decorated logic syntax. Similar case applies to the (tcomp) rule given in Figure 17.

4 The Decorated Logic for the state effect (L st )

The use and modification of the memory state is the fundamental feature of imperative languages, and considered as a sort of computational side effect. In this section, we present a proof system for the use of the global state which involves access and modify operations, called the decorated logic for the state effect (L st ). This logic is obtained by extending the generic framework presented in Section 3.2. In this case, the decoration (0) is reserved for pure terms, while (1) is for read-only (accessor) and (2) is for read-write (modifier) terms. Two terms are called strongly equal if they return the same result with the same state manipulation; they are called weakly equal if they return the same result with different state manipulations.

Figure 12 shows the grammar of the L st where 1 is the singleton type while V i is the type of values that can be stored in any location i. We assume that there is a set of locations called Loc. Given types X and Y, we have X × Y representing type products.

Terms are closed under composition (•) and pairing ( _, _ l ). I.e., for all terms f : X → Y and g : Y → Z, we have g • f : X → Z. Similarly, for all f : X → Y and g : X → Z, there is f, g l : X → Y × Z. Notice that the pair subscript 'l' denotes the left pairs. One can define in a symmetric way the right pairs for terms f : X → Y and g : X → Z as f, g r := permut • g, f l where permut := π 2 , π 1 l . In the same way, one can respectively obtain left and right products of terms f :

X 1 → Y 1 and g : X 2 → Y 2 as f × l g := f • π 1 , g • π 2 l and f × r g := f • π 1 , g • π 2 r .
The term pairs/products are used to impose some order of term evaluation since the evaluation result depends on the order that the mutable state is accessed/modified. I.e., the product of two terms can be intuitively interpreted as they run on the global state in parallel, while sequential products, put forward in (Dumas et al., 2014a, §2.3), enforce terms to use the state in sequence. The decoration of a pair/product depends on the decoration of its components, always taking the larger. I.e., ∀ f (0) : X → Y and Grammar of the decorated logic for the state:

(i ∈ Loc)

Types: t, s

::= X | Y | • • • | t × s | 1 | V i
Decorations for terms:

(d 1 ), (d 2 ) ::= (0) | (1) | (2) Terms: f, g ::= a (d) | b (d) | • • • | g • f (d) | f (d 1 ) : X → Y, g (d 2 ) : X → Z (max(d 1 ,d 2 )) l : X → Y × Z | lookup (1) i | update (2) i | (tpure • ) (0) Equations: eq ::= f (d) ≡ g (d) | f (d) ∼ g (d)
Figure 12:

L st : syntax g (2) : X → Z, the term f, g l : X → Y × Z takes the decoration (2).
Note that in L st , we do not necessarily stick to the sequential products, even pairs/products of modifiers (intuitively parallel execution of modifiers) are allowed to be constructed. However, they cannot be used in the provided equational reasoning, since they may lead to conflicts on the returned result due to possible hazardous parallel modifications of the global state. We can have equational reasoning only when the left component is at most an accessor. This restriction is given by the rules (w_lpair_eq) and (s_lpair_eq) in Figure 13. In the Coq implementation of this logic, as detailed in Section 4.2, we only allow the construction of pairs/products of modifiers under contradictory assumptions. See the constructor is_pair of the inductive type is.

The interface terms are lookup

i : 1 × S → V i and update i : V i × S → 1 × S
where S denotes the distinguished object of states which never appears in the decorated setting. The use of decorations provides a new schema where term signatures are constructed without any occurrence of the state object. For instance, lookup

i : 1 → V i is an accessor while update (2) i : V i → 1 is a modifier. This way, we keep signatures close to their syntax and compose compatible terms as usual. The term lookup reads the value stored in a given location while update modifies it. We can call them the unique sources of impurity, since only the terms including lookup or update are impure; meaning those do not include them are pure with respect to the state effect. The identity term id, the canonical pair projections π 1 , π 2 , the empty pair and constants are translated from a pure type system with type products using the tpure constructor, for all types X and Y, as follows:

id (0) X : X → X := tpure (λ x : X. x : X) π (0) 1 : X × Y → X := tpure fst π (0) 2 : X × Y → Y := tpure snd (0) X : X → 1 := tpure (λ x : X. void : 1) constant (0) x : 1 → X := tpure (λ _. x : X)
where fst and snd are constructors of product types. The intended model of the above grammar is built with respect to the set of states S where a pure term p (0) : X → Y is interpreted as a function p : X → Y, an accessor a (1) : X → Y as a function a : X × S → Y, and a modifier m (2) : X → Y as a function m : X × S → Y × S. The complete and detailed category theoretical model is given in (Ekici, 2015, §5.1). The syntax given in Figure 12 is enriched with two sets of rules Rules of the decorated logic for the state:

(pwrepl) f (d 1 ) 1 ∼ f (d 2 ) 2 : X → Y g (0) : Y → Z g (0) • f (d 1 ) 1 ∼ g (0) • f (d 2 ) 2 (wsubs) g (d 3 ) : X → Y f (d 1 ) 1 ∼ f (d 2 ) 2 : Y → Z f (d 1 ) 1 • g (d 3 ) ∼ f (d 2 ) 2 • g (d 3 ) (replsubs) f (d 1 ) 1 ≡ f (d 2 ) 2 : X → Y g (d 3 ) 1 ≡ g (d 4 ) 2 : Y → Z g (d 3 ) 1 • f (d 1 ) 1 ≡ g (d 4 ) 2 • f (d 2 ) 2 (w_unit) f (d 1 ) : X → 1 f (d 1 ) ∼ (0) X (ax 1 ) lookup (1) i • update (2) i ∼ id V i (0) (ax 2 ) ∀i, j ∈ Loc, i = j lookup (1) i • update (2) j ∼ lookup (1) i • (0) V j (effect) f (d 1 ) 1 , f (d 2 ) 2 : X → Y f (d 1 ) 1 ∼ f (d 2 ) 2 (0) Y • f (d 1 ) 1 ≡ (0) Y • f (d 2 ) 2 f (d 1 ) 1 ≡ f (d 2 ) 2 (local_global) f (d 1 ) 1 , f (d 2 ) 2 : X → 1 ∀ i ∈ Loc, lookup (1) i • f (d 1 ) 1 ∼ lookup (1) i • f (d 2 ) 2 f (d 1 ) 1 ≡ f (d 2 ) 2 (w_lpair_eq) f (d 1 ) 1 : X → Y f (d 2 ) 2 : X → Z d 1 ∈ {0, 1} π (0) 1 • f 1 , f 2 (max(d 1 ,d 2 )) l ∼ f (d 1 ) 1 (s_lpair_eq) f (d 1 ) 1 : X → Y f (d 2 ) 2 : X → Z d 1 ∈ {0, 1} π (0) 2 • f 1 , f 2 (max(d 1 ,d 2 )) l ≡ f (d 2 ) 2 Figure 13: L st : rules
presented in Figures 13 and11. Weak equalities do not form a congruence: the term replacement cannot be done unless the replaced term is pure. I.e., given an equation f

(d 1 ) 1 ∼ f (d 2 )
2 : X → Y and a term g : Y → Z, it is possible to get the equation g • f 1 ∼ g • f 2 only when the term g is pure. At this stage, we have no information about the modifications that f 1 and f 2 make on the memory state. Therefore, the post executed impure term g would destroy this result equality, for instance by reading the location i on which f 1 and f 2 has performed different modifications (pwrepl). However, the term substitution can be done regardless of the term decoration. I.e., given the equation f

(d 1 ) 1 ∼ f (d 2 ) 2 : Y → Z and a term g (d 3 ) : X → Y, it is possible to get the equation f 1 • g ∼ f 2 • g independent
from the decoration of the term g. We already now that f 1 and f 2 return the same result, executing any term g in advance would not end them returning different results (wsubs). Strong equalities form a congruence by allowing both term substitutions and replacements independent from the term decorations (replsubs).

Any term f : X → 1 with no result returned "void" (the unique inhabitant of 1 type) has an obvious result equality with the canonical empty pair X (w_unit).

The fundamental equations are given with the rules (ax 1 ) and (ax 2 ). The former states that by updating the location i with a value v and then observing the same location, one gets the value v. This outputs the same value with the identity term id V i , if it takes v as an argument. However, notice that these two ways of getting the value v have different state manipulations which makes them weakly equal. The latter, (ax 2 ), is to assume that updating the location j with a value v and then reading the content of a different location i would return the same value with first throwing out the value v then observing the content of the location i. They have different manipulations on the state so that they are weakly equal.

Two modifiers f

(2)

1 , f (2)
2 : X → Y modify the state in the same way if and only if

Y • f 1 ≡ Y • f 2 : X → 1, where Y : Y → 1 throws out the returned value. So that f (2) 1 , f (2) 2 : X → Y are strongly equal if and only if f 1 ∼ f 2 and Y • f 1 ≡ Y • f 2 (effect).
Notice that this rule is valid also for the other decorations of terms f 1 and f 2 .

Locally, the strong equality between two modifiers f

(2)

1 , f (2)
2 : X → 1 can also be expressed as a pair of weak equations:

f 1 ∼ f 2 and ∀i :Loc, lookup i • f 1 ∼ lookup i • f 2 .
The latter intuitively means that f 1 and f 2 leaves the memory with the same values stored in all (finitely many) locations after being executed.

Given that both return "void" there is no explicitly need to check if

f 1 ∼ f 2 . It suffices to see whether ∀i :Loc, lookup i • f 1 ∼ lookup i • f 2 to end up with f 1 ≡ f 2 (local_global).
The rule is valid also for the other decorations of terms f 1 and f 2 . With (w_lpair_eq) and (w_rpair_eq) term pairs are characterized: the (left) pair structure f 1 , f 2 l cannot be used when f 1 and f 2 , both are modifiers, since it may lead to a conflict on the returned result. However, it can be used only when f 1 is an accessor. We state by (w_lpair_eq

) that f 1 , f 2 (max(d 1 ,d 2 )) l has only result equality with f (d 1 )
1 and by (w_rpair_eq) that it has both result and effect equality with f

(d 2 )
2 . These rules are designed to be sound with respect to a categorical model detailed in (Ekici, 2015, §5.2, §5.3, §5.4, §5.5). However, their syntactic completeness is not immediate. [START_REF] Dumas | Relative hilbert-post completeness for exceptions[END_REF] defines a new syntactic completeness property, subsuming a consistency check, called the relative Hilbert-Post completeness. In (Ekici, 2015, §5.4), it is proven that this set of rules is complete with due respect.

Decorated properties of the memory state

In (Plotkin and Power, 2002, §3), an equational representation of the mutable state has been introduced. The decorated version of such representation is given as follows:

(1) d Annihilation lookup-update. Reading the content of a location i and then updating it with the obtained value is just like doing nothing. ∀ i ∈ Loc, update

(2)

i • lookup (1) i ≡ id (0) 1 : 1 → 1.
(2) d Interaction lookup-lookup. Reading twice the same location i is the same as reading it once.

∀ i ∈ Loc, lookup (1) i •
(0)

V i • lookup (1) i ≡ lookup (1) i : 1 → V i .
(3) d Interaction update-update. Storing value the values x and y in a row to the same location i is just like storing y in it.

∀ i ∈ Loc, update (2)
i • π (0) 2 • (update (2) i × r id (0) V i ) ≡ update (2) i •π (0) 2 : V i × V i → 1.
(4) d Interaction update-lookup. Storing the value x in a location i and then reading the content of i, one gets the value x.

∀ i ∈ Loc, lookup (1)
i • update (2) i ∼ id (0) V i : V i → V i . (5) d Commutation lookup-lookup.
The order of reading two different locations i and j does not matter.

∀ i = j ∈ Loc, (id (0) V i × r lookup (1) j ) • π -1(0) 1 • lookup (1) i ≡ permut (0) j,i • (id (0) V j × r lookup (1) i ) • π -1(0) 1 • lookup (1) j : 1 → V i × V j where π -1(0) 1 := id, (0) l .
(6) d Commutation update-update. The order of storing in two different locations i and j does not matter.

∀ i = j ∈ Loc, update

(2)

j • π (0) 2 • (update (2) i × r id (0) V j ) ≡ update (2) i • π (0) 1 • (id (0) V i × l update (2) j ) :V i × V j → 1.
(7) d Commutation update-lookup. The order of storing in a location i and reading another location j does not matter. ∀ i = j ∈ Loc, lookup

(1)

j • update (2) i ≡ π (0) 2 • (update (2) i × r id (0) V j ) • (id (0) V i × l lookup (1) j ) • π -1(0) 1 : V i → V j .
(8) d Commutation lookup-constant. Just after storing a constant c in a location i, observing the content of i is the same as regenerating the constant c.

∀ i ∈ Loc, ∀ c ∈ V i ; lookup (1) i • update (2) i • constant c (0) ≡ constant c (0) • update (2) i • constant c (0) : 1 → V i .
These are the archetype properties that we have proved within the scope of the logic L st . To see these proofs, check out author's PhD thesis (Ekici, 2015, §5.3). Besides, we have implemented the L st in Coq to certify mentioned proofs. Section 4.2 details this implementation.

L st in Coq

In this section, we aim to highlight some crucial points of the L st implementation in Coq. It mainly consists of four steps: (1) implementing the terms, (2) assigning the decorations over terms, (3) stating the rules, and (4) proving properties of the memory state referred in Section 4.1.

We represent the set of memory locations by a Coq parameter Loc : Type. Since memory locations may contain different types of values, we also assume an arrow type Val : Loc → Type that is the type of values contained in each location. This fixes a type for every location. Note that the system thus does not support reasoning about strong updates.

Parameters (Loc: Type) (Val: Loc → Type).
We define the terms of L st using an inductive predicate called term. It establishes a new Coq Type out of two input Types. The type term Y X is dependent. It depends on the Type instances X and Y, and represents the arrow type X → Y in the decorated framework. As opposed to a flat grammar with a typing predicate, we prefer a dependently typed implementation for higher readability.

Inductive term: Type

→ Type → Type | tpure: ∀ {X Y: Type}, (X → Y) → term Y X | comp: ∀ {X Y Z: Type}, term X Y → term Y Z → term X Z | pair: ∀ {X Y Z: Type}, term X Z → term Y Z → term (X*Y) Z | lookup: ∀ i:Loc, term (Val i) unit | update: ∀ i:Loc, term unit (Val i). Infix "o" comp (at level 70).
The constructor tpure takes a Coq side (pure) function and translates it into the decorated environment.

The comp constructor deals with the composition of two compatible terms. I.e., given a pair of terms f : term X Y and g : term Y Z, then the composition f • g would be an instance of the type term X Z.

For the sake of conciseness, infix '•' is used to denote the term composition. Similarly, the (left) pair constructor is to constitute pairs of compatible terms. I.e., given f : term Y X and g : term Z X, we have pair f, g l : term (Y × Z) X. Instead of the symbol _, _ l , we use the keyword pair in the implementation.

The terms lookup and update come as no surprise; just that the singleton type 1 and the type of values V i are respectively called unit and Val i in the code. The terms such as the identity, the pair projections, the empty pair and the constant function can be derived from the native Coq functions with the use of tpure constructor as follows: Remark that id is overloaded: defined one (on the left) is the identity of the decorated logic while the other one is the identity of Coq's logic. The pair projections are named pi1 and pi2 while the unique mapping X from any type X to 1 is named forget in the implementation.

The decorations are enumerated under the new type called kind: pure (0), ro (1) and rw (2) and inductively assigned to terms via the predicate called is. This predicate builds a proposition out of a term and a decoration. I.e., ∀i : Loc, is ro (lookup i) is a Prop instance, ensuring that "lookup i" is an accessor.

Notice that on the paper, we always mention the decoration of a term as a superscript. However, with such a Coq implementation, we do not need to additionally carry that information with a term. Instead, we inject it inside the rules as predicates, and check if a rule is applicable or not via this information. See Remark 4.1.

Inductive kind pure | ro | rw. Inductive is: kind → ∀ X Y, term X Y → Prop | is_tpure: ∀ X Y (f: X → Y), is pure (@tpure X Y f) | is_comp: ∀ k X Y Z (f: term X Y) (g: term Y Z), is k f → is k g → is k (f o g) | is_pair: ∀ k X Y Z (f: term X Z) (g: term Y Z), is ro f → is k f → is k g → is k (pair f g) | is_lookup: ∀ i, is ro (lookup i) | is_update: ∀ i, is rw (update i) | is_pure_ro: ∀ X Y (f: term X Y), is pure f → is ro f | is_ro_rw: ∀ X Y (f: term X Y), is ro f → is rw f.
Any term that is built by the tpure constructor is pure (is_tpure). The decoration of any term composition depends on its components and always takes the upper decoration (pure < ro < rw). E.g., given a modifier term and a read-only term, their composition will be a modifier, as well. This trivially follows from (is_comp), (is_pure_ro) and (is_ro_rw): see Lemma 3.2, and the corresponding Coq proof here (iii) . The decoration of a (left) pair of terms also depends on its components always taking the upper with the restriction that the first component can at most be an accessor. This is also trivial given (is_pair), (is_pure_ro) and (is_ro_rw). See the Coq proof of this fact here (iv) . We declare that the term lookup is an accessor (is_lookup), and the term update is a modifier (is_update). The last two constructors (is_pure_ro) and (is_ro_rw) define the decoration hierarchies.

It is easy to derive that any tpure built term is pure. I.e., the purity proof of the first pair projection:

Lemma is_pi1 X Y: is pure (@pi1 X Y).

Proof. apply is_tpure. Qed.

We now state the rules up to weak and strong equalities by defining them in a mutually inductive way: mutuality here is used to enable the constructors including both weak and strong equalities. We use the (iii)

https://github.com/ekiciburak/decorated-logic-for-states-effect/blob/master/Decorations.v# L76-L79 (iv) https://github.com/ekiciburak/decorated-logic-for-states-effect/blob/master/Decorations.v# L81-L84

The rule tcomp states that the tpure constructor preserves the composition of pure terms up to the strong equality: one can first compose pure terms on Coq side (using higher order function compose) and then apply tpure constructor to translate them into decorated settings or can translate the terms first and then compose them in decorated settings.

Remark 4.1. In a decorated logic, it is crucial to verify the decorations of the terms in applying/rewriting a rule. If the rule is applicable for all decorations, then it is not necessary to check the decorations of terms which appear in that rule. Otherwise put, decoration checks are necessary only when the rule premise has restrictions over term decorations. I.e., see the constructor w_lpair_eq above. We apply the same strategy for the logics presented in Sections 5 and 6 when implementing them in Coq.

This framework allows us to express and prove, in Coq, the decorated versions of the properties mentioned in Section 4.1. E.g., the statement commutation update-update looks like:

(** Commutation update update **) Theorem CUU: ∀ i j: Loc, i =j → update j o (pi2 o (rprod (update i) (@id (Val j)))) == update i o (pi1 o (lprod (@id (Val i)) (update j))).
where

Definition permut {X Y}: term (X*Y) (Y*X) pair pi2 pi1. Definition rpair {X Y Z} (f: term Y X) (g: term Z X): term (Y*Z) X permut o pair g f. Definition lprod {X Y X' Y'} (f: term X X') (g: term Y Y'): term (X*Y) (X'*Y') pair (f o pi1) (g o pi2). Definition rprod {X Y X' Y'} (f: term X X') (g: term Y Y') permut o pair (g o pi2) (f o pi1).
The full Coq proofs of such properties can be found here (v) , and the entire implementation there (vi) .

5 The Decorated Logic for the exception effect (L exc )

Exception handling is provided by most modern programming languages to deal with anomalous or exceptional events which require special processing. In this section, we present a proof system for exceptions, which involves raising and handling operations, called the decorated logic for the exception effect (L exc ). This logic is obtained by extending the generic framework presented in Section 3.2. In this context, the decoration (0) is reserved for pure terms, while (1) is for propagators and (2) is for catchers.

A fundamental feature of the exceptions mechanism is the distinction between ordinary (non-exceptional) values and exceptions (or exceptional values). Two terms are called strongly equal if they behave the same on ordinary and exceptional values; they are called weakly equal if they behave the same on ordinary values but differently on exceptional ones. It has been shown by [START_REF] Dumas | A duality between exceptions and states[END_REF] that the core part of this proof system is dual to one for the state (L st ). Based on this nice duality, we build the logic L exc , and detail it in the following.

Grammar of the decorated logic for the exception:

(e ∈ EName)

Types: t, s ::= X | Y | • • • | t+s | O | EV e
Decoration for terms:

(d 1 ), (d 2 ) ::= (0) | (1) | (2) Terms: f, g ::= a (d) | b (d) | • • • | g • f (d) | [f (d 1 ) : X → Y | g (d 2 ) : Z → Y] l (max(d 1 ,d 2 )) : X + Z → Y | tag (1) e | untag (2) e | (↓ f) (1) | (tpure • ) (0) Equations: eq ::= f (d) ≡ g (d) | f (d) ∼ g (d)
Figure 14: L exc : syntax

Figure 14 shows the grammar of L exc where O is the empty (uninhabited) type while EV e is the type of parameters for each exception name e. We assume that there is a finite set of exception names called EName. Given types X and Y, we have X+Y denoting co-product (disjoint union or sum) types. Terms are closed under composition (•) and co-pairing ([_ | _] l ). I.e., for all terms f : X → Y and g : Y → Z, we have g • f : X → Z. Similarly, for all f : X → Y and g : Z → Y, there is [f | g] l : X+Z → Y. Notice that the co-pair subscript 'l' denotes the left co-pairs. One can define in a symmetric way the right co-pairs for terms f : X → Y and g :

Z → Y as [f | g] r := [g, f] l • permut where permut := [in 2 | in 1 ] l .
Similarly, one can respectively obtain left and right co-products (sums) of terms f :

X 1 → Y 1 and g : X 2 → Y 2 as f+ l g := [in 1 • f | in 2 • g] l and f+ r g := [in 1 • f | in 2 • g] r .
The decoration of a co-pair (co-product) depends on the decoration of its components, always taking the larger. I.e., ∀ f (0) : X → Z and g

(2) : Y → Z, [f | g] l : X+Y → Z takes the decoration (2).
Being dual to the pairs in L st (which impose an evaluation order), co-pairs in L exc are used to have case distinction among terms. Co-pairs of catchers are allowed to be constructed in the logic L exc . However, they cannot be used in the provided equational reasoning as they lead to ambiguous case distinctions over input exceptional arguments for the component terms. I.e., it is not obvious to which input argument the recovery would apply when both are exceptional. The intended (v) https://github.com/ekiciburak/decorated-logic-for-states-effect/blob/master/Proofs.v (vi) https://github.com/ekiciburak/decorated-logic-for-states-effect equational reasoning can be done only when the left term is at most a propagator. The restriction is given by the rules (w_lcopair_eq) and (s_lcopair_eq) in Figure 15.

The interface terms are tag e : EV e → O+E and untag e : O+E → EV e +E where E denotes the distinguished object of exceptions which never appears in the decorated setting. The use of decorations provides a new schema where term signatures are constructed without any occurrence of it. For instance, tag

e : EV e → O is a thrower while untag

(2) e : O → EV e is a catcher. This way, we keep signatures close to their syntax and compose compatible terms as usual. The term tag e encapsulates an ordinary value with an exception of name e while the term untag e recovers the value from the exceptional case.

The '↓' symbol denotes the downcast term that takes as input a term and prevents it from catching exceptions. It is used when to define the try/catch block in this setting. See Definition 5.2.

The identity term id, the canonical co-pair inclusions in 1 and in 2 , and the empty co-pair [ ] X (used to convert the type of input exceptional value into the given type; X in this case) are translated from a pure type system with sum types using the tpure constructor, for all types X and Y, as follows:

id (0) X : X → X := tpure (λ x : X. x : X) in (0) 1 : X → X+Y := tpure inl in (0) 2 : Y → X+Y := tpure inr [ ] (0)
X : O → X := tpure (λ _ : O. x : X)
where inl and inr are constructors of sum types, and in the definition of [ ] X , X is assumed to be inhabited. The intended model of the grammar of the logic L exc is built with respect to the set of exceptions E where a pure term p (0) : X → Y is interpreted as a function p : X → Y, a propagator pp (1) : X → Y as a function pp : X → Y+E, and a catcher c Definition 5.2. For each propagators f (1) : X → Y, g (1) : EV e → Y and each exception name e, the propagator try(f)catch(e ⇒ g) (1) is defined in three steps, as follows:

Catch(e ⇒ g) (2) := [ id (0) Y | g (1) • untag (2) e ] l : Y+O → Y Try(f)Catch(e ⇒ g) (2) := Catch(e ⇒ g) (2) • in (0) 1 Y,O • f (1) : X → Y try(f)catch(e ⇒ g) (1) := ↓ Try(f)Catch(e ⇒ g) (2) : X → Y
To handle an exception, the intermediate expressions Catch(e ⇒ g) and Try(f)Catch(e ⇒ g) are private catchers and the expression try(f)catch(e ⇒ g) is a public propagator: the downcast operator intuitively used to prevent try(f)catch(e ⇒ g) from catching exceptions with name e which might have been raised before its execution. Below we depict the try(f)catch(e ⇒ g) definition as a diagram:

Y in 1 Y,O id Y B B ↓ X f G G Y in 1 Y,O G G Y + O id Y g • untag e G G Y O in 2 Y,O y y untag e G G EV e g W W
This, inside the downcast, intuitively tells us that if the term f throws an exception, then within the Catch block using the case distinction, provided by the copair, the exception is handled via the untag (unhandled exception gets propagated) and the continuation is the execution of the term g. 15, that we provide on the top of L exc syntax. The definition of try(f)catch(e ⇒ g) corresponds to the Java mechanism for exceptions as in (Gosling et al., 2005, §14) and in [START_REF] Jacobs | A formalisation of java's exception mechanism[END_REF]) with the following control flow (where exc? means "is this value an exception?"): an abrupt termination returns an uncaught exception and a normal termination returns an ordinary value.

exc?

Y v v N B B abrupt f (1) exc? Y t t N B B untag (2) e normal exc? Y v v N B B abrupt g (1)
normal or abrupt Remark 5.3. The decorated terms throw (1) and throw/catch (1) stated in Definitions 5.1 and 5.2 will serve, in Section 7 (see the translator function dCmd), as interpretations of the IMP+Exc commands THROW and TRY/CATCH.

The syntax given in Figure 14 is enriched with two sets of rules presented in Figures 15 and11. Weak equalities do not form a congruence: the term substitution cannot be done unless the substituted term is pure. I.e., given the equation f

(d 1 ) 1 ∼ f (d 2 )
2 : Y → Z and a term g : X → Y, it is possible to get the equation Rules of the decorated logic for the exception:

(pwsubs) g (0) : X → Y f (d 1 ) 1 ∼ f (d 2 ) 2 : Y → Z f (d 1 ) 1 • g (0) ∼ f (d 2 ) 2 • g (0) (wrepl) f (d 1 ) 1 ∼ f (d 2 ) 2 : X → Y g (d 3 ) : Y → Z g (d 3 ) • f (d 1 ) 1 ∼ g (d 3 ) • f (d 2 ) 2 (replsubs) f (d 1 ) 1 ≡ f (d 2 ) 2 : X → Y g (d 3 ) 1 ≡ g (d 4 ) 2 : Y → Z g (d 3 ) 1 • f (d 1 ) 1 ≡ g (d 4 ) 2 • f (d 2 ) 2 (w_empty) f (d 1 ) : O → X f (d 1 ) ∼ [ ] (0) X (w_downcast) f (2) : Y → X (↓ f) (1) ∼ f (2) (eax 1 ) untag (2) e • tag (1) e ∼ id (0)
EV e (eax 2 ) ∀e 1 , e 2 ∈ EName, e 1 = e 2 untag

(2)

e 1 • tag
(1)

e 2 ∼ [ ] (0)
EV e 1

• tag

(1)

e 2 (eeffect) f (d 1 ) 1 , f (d 2 ) 2 : Y → X f (d 1 ) 1 ∼ f (d 2 ) 2 f (d 1 ) 1 • [ ] (0) Y ≡ f (d 2 ) 2 • [ ] (0) Y f (d 1 ) 1 ≡ f (d 2 ) 2 (elocal_global) f (d 1 ) 1 , f (d 2 ) 2 : O → X ∀ e ∈ EName, f (d 1 ) 1 • tag (1) e ∼ f (d 2 ) 2 • tag (1) e f (d 1 ) 1 ≡ f (d 2 ) 2 (w_lcopair_eq) f (d 1 ) 1 : X → Y f (d 2 ) 2 : Z → Y d 1 ∈ {0, 1} [f 1 | f 2 ] (max(d 1 ,d 2 )) • in 1 (0) ∼ f (d 1 ) 1 (s_lcopair_eq) f (d 1 ) 1 : X → Y f (d 2 ) 2 : Z → Y d 1 ∈ {0, 1} [f 1 | f 2 ] (max(d 1 ,d 2 )) • in 2 (0) ≡ f (d 2 ) 2 Figure 15: L exc : rules f 1 • g ∼ f 2
• g only when the term g is pure. At this stage, we have no information about the behaviors of f 1 and f 2 on exceptional values. Therefore, the pre-executed term g would destroy this result equality unless being pure, for instance, by throwing an exception of name e for which f 1 and f 2 perform different behaviors: say one is propagating, while the other is recovering from it (pwsubs). However, the term replacement can be done regardless of the term decoration. I.e., given the equation f

(d 1 ) 1 ∼ f (d 2 )
2 : X → Y and a term g (d 3 ) : Y → Z, it is possible to get the equation g • f 1 ∼ g • f 2 independent from the decoration of the term g. Since f 1 and f 2 behave the same on ordinary values, executing any term g after f 1 and f 2 would not end them behave different on ordinary values (wrepl). Strong equalities form a congruence by allowing both term substitutions and replacements regardless of the term decorations (replsubs).

Any term f : O → X with no input parameter has an equivalence on ordinary values with the empty co-pair [ ] X (w_empty). The rule (w_downcast) states that the term (↓ f) behaves as f, if the argument is ordinary. The fundamental equations are given with the rules (eax 1 ) and (eax 2 ). The former states that encapsulating an ordinary value with an exception of name e followed by an immediate recovery would be equivalent to "doing nothing" in terms of ordinary values. Clearly, this is only a weak equation since its sides behave different on exceptional values: left hand side may recover but right hand side definitely propagates. The latter, (eax 2 ), is to assume that encapsulating an ordinary value v with an exception of name e 2 and then trying to recover it from a different exception of name e 1 would just lead e 2 to be propagated. Similarly, if the ordinary value v is encapsulated with e 2 with no recovery attempt afterwards would again lead e 2 to be propagated. These two operations behave the same on ordinary values but different on exceptional ones. For instance, left hand side recovers the input value (encapsulated with the exception name e 1 ) while right hand side propagates it.

Two catchers f

(2)

1 , f (2)
2 : X → Y behave the same on exceptional values if and only if eeffect). The rule is valid also for the other decorations of terms f 1 and f 2 .

f 1 • [ ] X ≡ f 2 • [ ] X , where [ ] X : O → X throws out exceptional values. So that f (2) 1 , f (2) 2 : X → Y are strongly equal if and only if f 1 ∼ f 2 and f 1 • [ ] X ≡ f 2 • [ ] X (
Strong equality between two catchers f

(2)

1 , f (2)
2 : O → X can also be expressed as a pair of weak equations: f 1 ∼ f 2 and ∀e : ENname, f 1 • tag e ∼ f 2 • tag e .The latter intuitively means that f 1 and f 2 behaves the same on all (finitely many) exceptional values when executed. Given that both behave the same on ordinary arguments (due to (w_empty)), there is no explicitly need to check if f 1 ∼ f 2 . It suffices to see whether ∀e : EName, f 1 • tag e ∼ f 2 • tag e to end up with f 1 ≡ f 2 (elocal_global). This rule is valid also for the other decorations of terms f 1 and f 2 .

With (w_lcopair_eq) and (w_rcopair_eq), term co-pairs (sums) are characterized: the (left) co-pair structure [f 1 | f 2 ] l cannot be used when f 1 and f 2 , both are catchers, since it may lead to a conflict on exceptional values. When f 1 is a propagator, with (w-copair-eq), we assume that ordinary values of type X are treated by

[f 1 | f 2 ] (max(d 1 ,d 2 ))
l as they would be by f

(d 1 )
1 and with (s-copair-eq) that ordinary values of type Z and exceptional values are treated by

[f 1 | f 2 ] (max(d 1 ,d 2 ))
l as they would be by f

(d 2 ) 2 .
Similar to the ones of the logic L st , the rules of the logic L exc also designed to be sound with respect to a categorical model which is detailed in (Ekici, 2015, §6.2, §6.3, §6.4, §6.5). In [START_REF] Dumas | Relative hilbert-post completeness for exceptions[END_REF]), we prove that this set of rules is complete with respect to the notion of relative Hilbert-Post completeness.

Decorated properties of the exception effect

Similar to the one for the state effect presented in Section 4.1, we propose an equational representation of the exception effect with the following decorated equations:

(1) d Annihilation tag-untag. Untagging an exception of name e and then raising it again is just like doing nothing. ∀ e ∈ EName, tag

(1)

e • untag (2) e ≡ id (0) O : O → O.
(2) d Commutation untag-untag. Untagging two distinct exception names can be done in any order. ∀ e = r ∈ EName, (untag e + r id EV r ) (2) • in

(0) 2 • untag (2) r ≡ (id EV e + l untag r ) (2) • in (0) 1 • untag (2) e : O → EV e + EV r .
(3) d Propagator-propagates. A propagator term always propagates the exception.

∀ e ∈ EName, a (1) : X → Y, a (1) • [ ] (0) X • tag (1) e ≡ [ ] (0) Y • tag (1) e : EV e → Y.
(4) d Recovery. The parameter used for throwing an exception may be recovered.

∀ f (1) , g (1) : X → O, [ ] (0) Y • f (1) ≡ [ ] (0) Y • g (1) =⇒ f (1) ≡ g (1) =⇒ ∀ e ∈ EName, u (0) 1 , u (0) 2 : X → EV e , throw (1) e • u (0) 1 ≡ throw (1) e • u (0) 2 =⇒ u (0) 1 ≡ u (0) 2 : X → EV e .
(5) d Try. The strong equation is compatible with try/catch.

∀ e ∈ EName, a

(1) 1) : EV e → Y, a

1 , a (1) 2 : X → Y, b (
(1) (8) d Try 2 . An exception gets propagated, if the exception name is not pattern matched in catch.

1 ≡ a (1) 2 =⇒ try(a 1 )catch(e ⇒ b) (1) ≡ try(a 2 )catch(e ⇒ b) (1) : X → Y.
∀ (e = f) ∈ EName, u (0) : X → EV f , b (1) : EV e → Y, try(throw f • u)catch(e ⇒ b) (1) ≡ throw (1) f • u (0) : X → Y.
These are the archetype properties that we have proved within the scope of the L exc . To see these proofs, check out (Ekici, 2015, §6.7). Besides, we have implemented the L exc in Coq to certify mentioned proofs. Section 5.2 briefly discusses this implementation. Notice that the premise of the property (4) d is a very specific mono requirement. It intuitively says that if there is a strong equality between two propagators (i.e., f (1) and g (1) ) after removing the exceptional values they may propagate, then they are strongly equal. In the absence of this requirement the property is not valid.

L exc in Coq

Coq implementation of L exc follows the same approach with the one for L st as summarized in Section 4.2. We represent the set of exception names by a Coq parameter EName : Type. An arrow type EVal : EName → Type is assumed as the type of values (parameters) for each exception name. We then inductively define terms and assign decorations over them. There, we respectively use keywords epure, ppg and ctc instead of ( 0), ( 1) and ( 2). The rules up to weak and strong equalities are stated in a mutually inductive way to allow constructors including both types of equalities, similar to the approach presented in Section 4.2. We choose not to replay the entire Coq encoding here, but at least give Coq formalizations of Definitions 5.1 and 5. The encodings of other terms are contained in this file (vii) . We can conclude that such a framework allows us to express and prove, in Coq, the decorated versions of the properties mentioned in Section 5.1. E.g., the statement propagator-propagates looks like:

(** Propagator propagates **)

Lemma PPT: ∀ X Y (e: EName) (a: term Y X), is ppg a → a o ((@empty X) o tag e) == (@empty Y) o tag e.

The full Coq proofs of such properties can be found here (viii) , and the entire implementation there (ix) .

6 Combining L st and L exc

In order to formally cope with different computational effects, one needs to compose the related formal models. For instance, using monad transformers (Jaskelioff ( 2009)), it is usually possible to combine (vii) https://github.com/ekiciburak/decorated-logics-for-exceptions-effect/blob/master/Terms.v (viii) https://github.com/ekiciburak/decorated-logics-for-exceptions-effect/blob/master/Proofs.v (ix) https://github.com/ekiciburak/decorated-logics-for-exceptions-effect effects formalized by monads, as encoded in Haskell. Handler compositions allow combining effects modeled by algebraic handlers, as implemented in Eff by Bauer andPretnar (2015, 2014); [START_REF] Pretnar | Inferring algebraic effects[END_REF] and in Idris by [START_REF] Brady | Programming and reasoning with algebraic effects and dependent types[END_REF]. To combine effects formalized in decorated settings, we just need to compose the related logics. In this section, we formally study the combination of the state and the exception effects using the logics L st and L exc . We call the newly born logic the decorated logic for the state and the exception, and denote it L st+exc . To start with, we give the syntax of L st+exc below in Figure 16.

Grammar of the decorated logic for the state and the exception:

(i ∈ Loc) (e ∈ EName)
Types: t, s

::= X | Y | • • • | t × s | t+s | 1 | O | V i | EV e
Decoration for terms:

(d 1 , d 2 ), (d 3 , d 4 ) ::= (0, 0) | (0, 1) | (0, 2) | (1, 0) | (1, 1) | (1, 2) | (2, 0) | (2, 1) | (2, 2) Terms: f, g ::= a (d 1 ,d 2 ) | b (d 1 ,d 2 ) | • • • | g • f (d 1 ,d 2 ) | f (d 1 ,d 2 ) , g (d 3 ,d 4 ) (max(d 1 ,d 3 ),max(d 2 ,d 4 )) l | [f (d 1 ,d 2 ) | g (d 3 ,d 4 ) ] (max(d 1 ,d 3 ),max(d 2 ,d 4 )) l | lookup (1,0) i | update (2,0) i | tag (0,1) e | untag (0,2) e | (↓ f) (0,1) | (tpure • ) (0,0)
Equations:

eq ::= f (d 1 ,d 2 ) ≡≡ g (d 1 ,d 2 ) | f (d 1 ,d 2 ) ≡∼ g (d 1 ,d 2 ) | f (d 1 ,d 2 ) ∼≡ g (d 1 ,d 2 ) | f (d 1 ,d 2 ) ∼∼ g (d 1 ,d 2 )
Figure 16: L st+exc : syntax

The decorations are paired off to cover all possible combinations: the decoration symbol on the left is given in terms of the state effect while the one on the right is of the exception. I.e., f (1,2) says that f may access to the state alongside catching exceptions. The decoration of a (co)-pair/(co)-product or a composition depends on the decorations of its components, always taking the larger. I.e., ∀ f (1,2) : X → Y and g (2,1) : Y → Z, g • f : X → Z takes the decoration (2, 2). The pairs/products of compatible terms f

(2,2) 1 , g (2,2) 1
, and similarly the co-pair/co-products of compatible terms f

(2,2) 2 , g
(2,2) 2 can be constructed within the scope of L st+exc but cannot be used in the provided equational reasoning. This is because, f

(2,2) 1 and g

(2,2) 1 , as two modifiers, may lead to conflicts on the returned results over any type of (exceptional or ordinary) arguments due to the possible hazardous parallel modifications of the global state, while f (2,2) 2 and g

(2,2) 2 , as two catchers, may yield in ambiguous case distinctions over input exceptional arguments. I.e., it is not obvious to which input argument the recovery would apply when both are exceptional. The rules (w_lpair_eq), (s_lpair_eq), (w_lcopair_eq) and (s_lcopair_eq), in Figure 17, enforce these restrictions.

The types of L st+exc is the union of the types of L st and L exc . Similarly, the terms of L st+exc is the union of the terms of L st and L exc . The interface terms for the state effect are pure with respect to the exception and vice versa: lookup (1,0) , update (2,0) , tag (0,1) and untag (0,2) . As in Sections 4 and 5, we use the special tpure constructor to translate pure terms such as the identity id, the canonical pair projections π 1 , π 2 , the empty pair , the canonical co-pair inclusions in 1 , in 2 , the empty co-pair [ ] and constants from a pure type system with product and sum types using the tpure constructor, for all types X and Y, as:

id (0,0) X : X → X := tpure (λ x : X. x : X) π (0,0) 1 : X × Y → X := tpure fst π (0,0) 2 : X × Y → Y := tpure snd (0,0) X : X → 1 := tpure (λ x : X. void : 1) in (0,0) 1 : X → X+Y := tpure inl in (0,0) 2 : Y → X+Y := tpure inr [ ] (0,0) X : O → X := tpure (λ _ : O. x : X) constant (0,0) x : 1 → X := tpure (λ _. x : X)
where fst and snd are constructors of product types while inl and inr are of sum types, and in the definition of [ ] X , X is assumed to be inhabited.

The rule combinations need a bit of reformulation as we summarize below:

• The decoration symbol (0) freely converts into (1) and (2), while the symbol (1) just into (2) when the other symbol is fixed. I.e., f (0,2) freely converts into f (1,2) . See all cases below:

- f (0,d) f (1,d) , f (1,d) f (2,d) , f (d,0) f (d,1) , f (d,1) f (d,2) for d ∈ {0, 1, 2}
• We have all possible combinations of equality sorts: ≡≡, ≡∼, ∼≡ and ∼∼. The first equality symbol relates terms with respect to the state effect. I.e., f ≡∼ g means that f and g are strongly equal with respect to the state, while being weakly equal with respect to the exception. Below we present the conversion rules between these four sorts. The burden here is that a strong equality symbol can always be freely converted into a weak one independent of according to which effect it relates terms. But, to convert a weak equality symbol into a strong one, we need to make sure that the related terms are decorated either with (0) or (1) with respect to the effect they are weakly related.

-(≡≡-to-≡∼) 2) , (≡≡-to-∼≡) 2) , (∼≡-to-∼∼) 2) , (≡∼-to-≡≡) 2) , (∼∼-to-∼≡)

f (2,2) ≡≡ g (2,2) f (2,2) ≡∼ g (2,
f (2,2) ≡≡ g (2,2) f (2,2) ∼≡ g (2,2) -(≡∼-to-∼∼) f (2,2) ≡∼ g (2,2) f (2,2) ∼∼ g (2,
f (2,2) ∼≡ g (2,2) f (2,2) ∼∼ g (2,2) -(∼≡-to-≡≡) f (1,2) ∼≡ g (1,2) f (1,2) ≡≡ g (1,
f (2,1) ≡∼ g (2,1) f (2,1) ≡≡ g (2,1) -(∼∼-to-≡∼) f (1,2) ∼∼ g (1,2) f (1,2) ≡∼ g (1,
f (2,1) ∼∼ g (2,1) f (2,1) ∼≡ g (2,1)
• The rules of the logic L st+exc are presented in Figure 17 as a union of the ones given in Figures 13 and 15 in terms of new equality sorts and refined term decorations. There, we replay the whole rule bodies, and implicitly assume that all equality sorts are equivalence relations respecting the properties reflexivity, symmetry, and transitivity.

We plan it as a future work to come up with a more general and systematic way to combine effects formalized within decorated logics.

Rules of the decorated logic for the state and the exception:

(assoc) f (d 1 ,d 2 ) : X → Y g (d 3 ,d 4 ) : Y → Z h (d 5 ,d 6 ) : Z → T h (d 5 ,d 6 ) • (g (d 3 ,d 4 ) • f (d 1 ,d 2 ) ) ≡≡ (h (d 5 ,d 6 ) • g (d 3 ,d 4 ) ) • f (d 1 ,d 2 ) (ids) f (d 1 ,d 2 ) : X → Y f (d 1 ,d 2 ) • id (0,0) X ≡≡ f (d 1 ,d 2 ) (idt) f (d 1 ,d 2 ) : X → Y id (0,0) Y • f (d 1 ,d 2 ) ≡≡ f (d 1 ,d 2 ) (pwrepl) f (d 1 ,d 2 ) 1 ∼≡ f (d 3 ,d 4 ) 2 : X → Y g (0,d 5 ) : Y → Z g (0,d 5 ) • f (d 1 ,d 2 ) 1 ∼≡ g (0,d 5 ) • f (d 3 ,d 4 ) 2 (wsubs) g (d 5 ,d 6 ) : X → Y f (d 1 ,d 2 ) 1 ∼≡ f (d 3 ,d 4 ) 2 : Y → Z f (d 1 ,d 2 ) 1 • g (d 5 ,d 6 ) ∼≡ f (d 3 ,d 4 ) 2 • g (d 5 ,d 6 ) (pwsubs) g (d 5 ,0) : X → Y f (d 1 ,d 2 ) 1 ≡∼ f (d 3 ,d 4 ) 2 : Y → Z f (d 1 ,d 2 ) 1 • g (d 5 ,0) ≡∼ f (d 3 ,d 4 ) 2 • g (d 5 ,0) (wrepl) f (d 1 ,d 2 ) 1 ≡∼ f (d 3 ,d 4 ) 2 : X → Y g (d 5 ,d 6 ) : Y → Z g (d 5 ,d 6 ) • f (d 1 ,d 2 ) 1 ≡∼ g (d 5 ,d 6 ) • f (d 3 ,d 4 ) 2 (replsubs) f (d 1 ,d 2 ) 1 ≡≡ f (d 3 ,d 4 ) 2 : X → Y g (d 5 ,d 6 ) 1 ≡≡ g (d 7 ,d 8 ) 2 : Y → Z g (d 5 ,d 6 ) 1 • f (d 1 ,d 2 ) 1 ≡≡ g (d 7 ,d 8 ) 2 • f (d 3 ,d 4 ) 2 (w_unit) f (d 1 ,d 2 ) : X → 1 f (d 1 ,d 2 ) ∼≡ (0,0) X (w_empty) f (d 1 ,d 2 ) : O → X f (d 1 ,d 2 ) ≡∼ [ ] (0,0) X (w_downcast) f (d 1 ,2) : Y → X (↓ f) (d 1 ,1) ≡∼ f (d 1 ,2) (ax 1 ) lookup (1,0) i • update (2,0) i ∼≡ id (0,0) V i (ax 2 ) ∀i, j ∈ Loc, i = j lookup (1,0) i • update (2,0) j ∼≡ lookup (1,0) i • (0,0) V i (eax 1 ) untag (0,2) e • tag (0,1) e ≡∼ id (0,0) EV e (eax 2 ) ∀e 1 , e 2 ∈ EName, e 1 = e 2 untag (0,2) e 1 • tag (0,1) e 2 ≡∼ [ ] (0,0) EV e • tag (0,1) e 2 (effect) f (d 1 ,d 2 ) 1 , f (d 3 ,d 4 ) 2 : X → Y f (d 1 ,d 2 ) 1 ∼≡ f (d 3 ,d 4 ) 2 (0,0) Y • f (d 1 ,d 2 ) 1 ≡≡ (0,0) Y • f (d 3 ,d 4 ) 2 f (d 1 ,d 2 ) 1 ≡≡ f (d 3 ,d 4 ) 2 (eeffect) f (d 1 ,d 2 ) 1 , f (d 3 ,d 4 ) 2 : Y → X f (d 1 ,d 2 ) 1 ≡∼ f (d 3 ,d 4 ) 2 f (d 1 ,d 2 ) 1 • [ ] (0,0) Y ≡≡ f (d 3 ,d 4 ) 2 • [ ] (0,0) Y f (d 1 ,d 2 ) 1 ≡≡ f (d 3 ,d 4 ) 2 (local_global) f (d 1 ,d 2 ) 1 , f (d 3 ,d 4 ) 2 : X → 1 ∀ i ∈ Loc, lookup (1,0) i • f (d 1 ,d 2 ) 1 ∼≡ lookup (1,0) i • f (d 3 ,d 4 ) 2 f (d 1 ,d 2 ) 1 ≡≡ f (d 3 ,d 4 ) 2 (elocal_global) f (d 1 ,d 2 ) 1 , f (d 3 ,d 4 ) 2 : O → X ∀ e ∈ EName, f (d 1 ,d 2 ) 1 • tag (0,1) e ≡∼ f (d 3 ,d 4 ) 2 • tag (0,1) e f (d 1 ,d 2 ) 1 ≡≡ f (d 3 ,d 4 ) 2 (w_lpair_eq) f (d 1 ,d 2 ) 1 : X → Y f (d 3 ,d 4 ) 2 : X → Z d 1 ∈ {0, 1} π (0,0) 1 • f 1 , f 2 ((max(d 1 ,d 3 ),max(d 2 ,d 4 )) l ∼≡ f (d 1 ,d 2 ) 1 (s_lpair_eq) f (d 1 ,d 2 ) 1 : X → Y f (d 3 ,d 4 ) 2 : X → Z d 1 ∈ {0, 1} π (0,0) 2 • f 1 , f 2 ((max(d 1 ,d 3 ),max(d 2 ,d 4 )) l ≡≡ f (d 3 ,d 4 ) 2 (w_lcopair_eq) f (d 1 ,d 2 ) 1 : X → Y f (d 3 ,d 4 ) 2 : Z → Y d 2 ∈ {0, 1} [f 1 | f 2 ] ((max(d 1 ,d 3 ),max(d 2 ,d 4 )) • in 1 (0,0) ≡∼ f (d 1 ,d 2 ) 1 (s_lcopair_eq) f (d 1 ,d 2 ) 1 : X → Y f (d 3 ,d 4 ) 2 : Z → Y d 2 ∈ {0, 1} [f 1 | f 2 ] ((max(d 1 ,d 3 ),max(d 2 ,d 4 )) • in 2 (0,0) ≡≡ f (d 3 ,d 4 ) 2 (tcomp) f (p,p) : Y → Z g (p,p) : X → Y (tpure f) (0,0) • (tpure g) (0,0) ≡≡ (tpure (f • g)) (0,0)

Decorated properties of the state and exception effects

The properties given in Sections 4.1 and 5.1 are now stated with the refined term decorations, and related with the equation sort ≡≡. I.e., the statements propagator-propagates and update-update look like:

∀ e ∈ EName, a (0,1) : X → Y, a (0,1) • [ ] (0,0) X • tag (0,1) e ≡≡ [ ] (0,0) Y • tag (0,1) e : EV e → Y. ∀ i = j ∈ Loc, update (2,0) j • π (0,0) 2 • (update (2,0) i × r id (0,0) V j ) ≡≡ update (2,0) i • π (0,0) 1 • (id (0,0) V i × l update (2,0) j ) : V i × V j → 1.
These are the archetype properties that we can prove within the scope of the L st+exc . Although it is doable, we prefer not to prove them for this generic framework (skipped since it would take substantial amount of time); instead, we first specialize them in a way to serve as a target language for a denotational semantics of IMP+Exc, and then prove them for the specialized version. Also, we encode the specialized version in Coq and certify related proofs. Section 7 gives the related details.

7 IMP+Exc over the combined decorated logic L st+exc Now, it comes to define a denotational semantics for the IMP+Exc language, with the combined decorated logic for the state and the exception (L st+exc ) as the target language. Recall that by doing this, we aim to prove some (strong) equalities between terminating programs written in IMP+Exc with respect to the state and the exception effects.

In IMP+Exc, the values that can be stored in any location (variable) i are just integers. So that any occurrence of (V i ) in term signatures of L st+exc is replaced by Z. I.e., lookup (1,0) : 1 → Z and update (2,0) : Z → 1. We now define a denotational semantics of IMP+Exc expressions over combined decorated settings using two translator functions daExp and dbExp. The former takes an arithmetic expression as input and outputs a decorated term of type term Z 1, while the latter takes a Boolean expression and returns a decorated term of type term B 1:

daExp n ⇒ (constant n) (0,0) daExp x ⇒ (lookup x ) (1,0) daExp (a 1 +a 2 ) ⇒ (tpure add) (0,0) • daExp a 1 , daExp a 2 (d,0) l daExp (a 1 × a 2 ) ⇒ (tpure mlt) (0,0) • daExp a 1 , daExp a 2 (d,0) l daExp (a 1 -a 2 ) ⇒ (tpure subt) (0,0) • daExp a 1 , daExp a 2 (d,0) l dbExp b ⇒ (constant b) (0,0) dbExp (a 1 ? = a 2 ) ⇒ (tpure chkeq) (0,0) • daExp a 1 , daExp a 2 (d,0) l dbExp (a 1 ? = a 2 ) ⇒ (tpure chkneq) (0,0) • daExp a 1 , daExp a 2 (d,0) l dbExp (a 1 ? > a 2 ) ⇒ (tpure chkgt) (0,0) • daExp a 1 , daExp a 2 (d,0) l dbExp (a 1 ? < a 2 ) ⇒ (tpure chklt) (0,0) • daExp a 1 , daExp a 2 (d,0) l dbExp (b 1 ∧ b 2 ) ⇒ (tpure andB) (0,0) • dbExp b 1 , dbExp b 2 (d,0) l dbExp (b 1 ∨ b 2 ) ⇒ (tpure orB) (0,0) • dbExp b 1 , dbExp b 2 (d,0) l dbExp (¬b) ⇒ (tpure notB) (0,0) • dbExp b (d,0)
In "dbExp b" (6 th line above on the left), b can be either of the Boolean expressions true and false. The constructor tpure is applied to given unary and binary functions. For instance add : (Z × Z) → Z takes an instance of an integer tuple and returns their sum. To see the definition of these functions in a Coq implementation, please check out this file (x)

d := let f (d 1 ,0) = daExp(a 1 ) in let g (d 2 ,0) = daExp(a 2 ) in max(d 1 , d 2 ).
The same strategy follows for Boolean expressions, too.

We have some additional rules to make use of some pure algebraic operations in the combined decorated setting presented in Figure 18 where the pure term lpi b f : 1 → 1, within the rule (imp-li), is used to bridge successive loop iterations as long as the loop conditional evaluates into decorated logic's true (constant true). Also, the pure term pbl : B → 1+1 forms a bridge between the usual Boolean data type and its correspondence in the decorated settings which is the type 1+1.

lpi (b : term 1 (1 + 1)) (f : term 1 1) := tpure (λ x : 1.x). such that void : 1 is the unique constructor of the type 1, and inl, inr : 1 → (1 + 1) are the canonical inclusions.

The rule (imp 6 ) (functional extensionality), in Figure 18, is to say that if two pure functions on Coq side are point-wise equal, then they are strongly equal in the decorated setting. Here we take them strongly equal since strong and weak equalities are indistinguishable when the related terms are pure. The idea is to be able to use Coq's Leibniz equality as the strong equality in the decorated setting. Note also that in (imp 2 ) and (imp 4 ) by replacing false into true we get (imp 3 ) and (imp 5 ) that are not explicitly stated in Figure 18.

Lemma 7.2. pbl (0,0) • (constant f alse) (0,0) ≡≡ in 2 .

Proof: unfolding all term definitions, we have tpure (λ b : bool. if b then (inl void) else (inr void))

• tpure (λ _ : void.true) ≡≡ tpure inl. Now, we obtain ∀x : 1, inl void = inl x by first rewriting tcomp from left to right, and then applying imp 6 which is trivial since Leibniz equality '=' is reflexive.

Lemma 7.3. pbl (0,0) • (constant true) (0,0) ≡≡ in 1 .

(x) https://github.com/ekiciburak/impex-on-decorated-logic/blob/master/Functions.v (imp 1 ) ∀p, q : Z, (f : replace EV e and Y with 1. This means that we stick to a single exceptional value (parameter), for each exception name e ∈ EName.

Z × Z → Z) tpure f • constant p, constant q l ≡≡ (constant f(p, q)) (imp 2 ) ∀p, q : Z, (f : Z × Z → B) f(p, q) = false tpure f • constant p, constant q l ≡≡ constant false (imp 4 ) ∀p, q : B, (f : B × B → B) f(p, q) = false tpure f • constant p, constant q l ≡≡ constant false (imp -li) ∀(b : term 1 (1 + 1)) (f : term 1 1) lpi b f ≡≡ (lpi b f) • f id l • b (imp 6 ) (∀x, f x = g x) tpure f ≡ tpure g
Below, we recursively define the IMP+Exc commands within L st+exc using a translator function dCmd which establishes a decorated term of type term 1 1 out of an input command: 0) dCmd (THROW e) ⇒ throw e (0,1)

dCmd (SKIP) ⇒ (id 1) (0,0) dCmd (x a) ⇒ (update x ) (2,0) • (daExp a) (d 1 ,0) dCmd (c 1 ; c 2 ) ⇒ (dCmd c 2 ) (d 1 ,d 2 ) • (dCmd c 1 ) (k 1 ,k 2 ) dCmd (if b then c 1 else c 2 ) ⇒ dCmd c 1 dCmd c 2 (d 1 ,d 2 ) l • pbl (0,0) • (dbExp b) (d 3 ,0) dCmd (while b do c) ⇒ (lpi (pbl • (dbExp b)) (dCmd c)) • (dCmd c) id (d 1 ,d 2 ) l • pbl (0,0) • (dbExp b) (d 3 ,
dCmd (TRY c 1 CATCH e ⇒ c 2 ) ⇒ try (dCmd c 1 ) catch (e ⇒ (dCmd c 2 )) (d 1 ,d 2 )
Remark 7.5. To calculate the decorations d 1 and d 2 (or k 1 and k 2 ), we use the following strategy:

d 1 := let f (d 1 ,d 2 ) = dCmd(c 1 ) in let g (d 3 ,d 4 ) = dCmd(c 2 ) in max(d 1 , d 3 ). d 2 := let f (d 1 ,d 2 ) = dCmd(c 1 ) in let g (d 3 ,d 4 ) = dCmd(c 2 ) in max(d 2 , d 4 ).
(xi) https://github.com/ekiciburak/impex-on-decorated-logic/blob/master/Derived_co_Pairs.v#L122-L133

For the strategy to calculate d 3 , see Remark 7.1. Also, recall Definition 5.2: translation of any IMP+Exc command cannot be a public catcher, even the one for TRY/CATCH. Thus, dCmd function outputs terms at most wih decoration (1) with respect to the exception effect.

In Figure 19, the diagram on the left schematizes the command if b then c 1 else c 2 : if the Boolean expression dbExp b evaluates into (constant true) then by Lemma 7.3, we have the command c 1 in execution, c 2 otherwise by Lemma 7.2. As for the loops, it is well know that as long as the looping condition evaluates into (constant true), loop body gets executed. This is depicted in Figure 19 (the diagram on the right), as the arrow lpi b c is each time replaced by the whole diagram itself. The rule (imp-li) allows us to do so. If the looping condition evaluates into (constant false), using Lemma 7.2, we then have the term id 1 in execution forcing the loop to terminate. Recall that the case distinction in the diagrams are provided by the term inclusions. 1 We now encode the IMP+Exc denotational semantics, with the L st+exc as the target language, in Coq. Arithmetic and Boolean expressions are inductively forming new Coq Types, called aExp and bExp respectively. As for the type constructors, we use the syntactic operators given as parts of aexp and bexp in Figure 2. The difference lies in the naming: notations are translated into plain text. It is easy to match them one another as they are given in the same order. Notice also that the implementation of the constant Boolean expressions true and false are subsumed by the constructor bconst. We interpret the functions daExp and dbExp in Coq using following fixpoints: We follow a similar idea to implement commands. We inductively define a Coq type Cmd of IMP+Exc commands whose constructors are the members of IMP+Exc command set as presented in Figures 2 and6. Notice that some commands are encoded with different names. I.e., the assignment command ' ' is called assign, the sequencing command ';' is called sequence while "if then else" block is named cond in the implementation. It is easy to match them one another since they are presented in the same order. We now interpret the dCmd function in Coq using the below fixpoint: Now, we retain sufficient material to state and prove equivalences between programs written in IMP+Exc. Also, the discussed Coq implementation allows us to certfy them in Coq.

1 in 1 c 1 5 5 1 dbExp b G G B pbl G G 1 + 1 c 1 c 2 G G 1 1 in 2 y y c 2 Y Y 1 in 1 c G G 1 lpi b c Ò Ò 1 dbExp b G G B pbl G G 1 + 1 (lpi b c) • c id 1 G G 1 1 in 2 y y id 1 S S
tag e G G O [] 1 G G 1 1 in 1 id 1 B B 1 c 1 G G 1 in 1 G G 1 + O id 1 c 2 • untag e G G 1 O in 2 y y untag e G G 1 c 2 X X

Program equivalence proofs

In this section, we finally prove equivalences of several programs written in IMP+Exc, using the denotational semantics characterized within the scope of the logic L st+exc . Note that for the sake of simplicity, we will use u x , l x , (t op) and (c p) instead of (update x) (2,0) , (lookup x) (1,0) , (tpure op) (0,0) and (constant p) (0,0) , respectively.

Remark 7.6. Recall that the use of term products is to impose some order of term evaluation on the mutable state. IMP+Exc specific properties of the mutable state are slightly different than their generic versions (mentioned in Section 4.1) due to the fact that the language does not allow parallel term evaluations, meaning that every term is evaluated in the given sequence. Therefore, we no more need to use term products in property statements. The properties we use through out the following proofs are re-stated in Figure 21. The full certified Coq proofs of these properties can be found here (xii) .

1. interaction update-update ∀ x ∈ Loc p, q : Z, u x • (c p) • u x • (c q) ≡≡ u x • (c p) 2. commutation update-update ∀ x = y ∈ Loc p, q : Z, u x • (c p) • u y • (c q) ≡≡ u y • (c q) • u x • (c p) 3. commutation-lookup-constant-update ∀ x ∈ Loc, p, q ∈ Z, l x , (c q) l • u x • (c p) ≡≡ (c p), (c q) l • u x • (c p)
Figure 21: Primitive properties of the state: IMP+Exc specific Remark 7.7. Below, we state three lemmata using the IMP+Exc notation introduced in Figures 2 and6. However, we introduce a new set of notations for the Coq encoding to increase the readability score: browse this set of notations here (xiii) where, i.e., the assign command is denoted by '::=' while the sequence command by '; ;'. These notations do not appear through out the paper, but might be of help in reading the lemma statements in the Coq encoding. Notice also that they are not so pretty, due to the fact that Coq internally reserves prettier notations for other issues.

Another point here to notice is that the proofs in the following might be long and hard to follow. If you find it so, please try reading the Coq codes. They are written in parallel with the ones on the paper. Starting from Lemma 7.10, we give overall explanations about the way we compute the proof using our semantics (xii) https://github.com/ekiciburak/impex-on-decorated-logic/blob/master/Proofs.v xiii) https://github.com/ekiciburak/impex-on-decorated-logic/blob/master/IMPEX_to_COQ.v#L185-L205

before diving it into the detailed rule applications. Note also that proofs are chosen to be presented in a way that the sides of the equations are simplified until obtaining a trivial equation to solve. Remark 7.8. All the statements we prove below are strong equations. The reason is that IMP+Exc (or IMP) language does not have a return command. Thus, one cannot compare the values that two programs return. When we use some combined decorated logic as a target language for the semantics of another language with the return command (i.e., the C language), then it would make sense to prove sentences with weak equations. Recall also that any strong equation can be seen as a weak equation.

Lemma 7.9. For all exceptionally pure commands f, g (doesNotThrowTC (f) = true, doesNotThrowTC (g) = true) and b ∈ {true, false}, if program pieces prog1 and prog2 are given as in the following listings, then dCmd (prog1) ≡≡ dCmd (prog2).

Listing 1: prog1 Note that the function doesNotThrowTC : cmd → Bool takes any command, recursively checks whether the input involves either THROW or TRY/CATCH, and returns true if that is the case; false otherwise. Browse this function, in a Coq implementation, here (xiv) .

Proof: We sketch the diagrams of both programs below:

1 in 1 f 3 3 1 c b G G B pbl G G 1 + 1 f g G G 1 1 in 2 y y g a a 1 in 1 k 3 3 1 c b G G B pbl G G 1 + 1 k g G G 1 1 in 2 y y g a a
where k = (if b then f else g). The statement we would like to prove is

f g l • pbl • c b ≡≡ k g l • pbl • c b. (1)
Using the rules of the logic L st+exc , in the below given order, the idea is to simplify both sides of the statement into the same shape with respect to the equality sort ≡≡. The proof proceeds by a case analysis on b.

If b = false, by unfolding the definitions of pbl and (c f alse), we have

f g l • t (bool_to_two) • t (λ x : unit.false) ≡≡ k g l • t (bool_to_two) • t (λ x : unit.false).
(2) We rewrite (tcomp) on both sides, and get f g l • t (λ x : unit.bool_to_two false) ≡≡ k g l • t (λ x : unit.bool_two false).

(3) (xiv) https://github.com/ekiciburak/impex-on-decorated-logic/blob/master/IMPEX_to_COQ.v#L148

Since, there is no exceptional case, we are freely back to ≡≡. By rewriting commutation -lookup -constant -update, we obtain

(lpi b f) • u x • (t +) • c 2, c 4 • u x • (c 2) ≡≡ u x • (c 14). (16)
The rule (imp 1 ) gives

(lpi b f) • u x • (c 6) • u x • (c 2) ≡≡ u x • (c 14). (17)
Now, we rewrite the lemma interaction-update-update (see Figure 21) and get

(lpi b f) • u x • (c 6) ≡≡ u x • (c 14). ( 18
)
2. For the second loop iteration, rewriting (imp-li) gives

(lpi b f) • f id 1 • pbl • (t ? <)• l x , (c 11) • u x • (c 6) ≡≡ u x • (c 14). ( 19
)
where looping pre-condition evaluates into (c true). Therefore, we iterate the above procedure, given in the step 1, once again and derive

(lpi b f) • u x • (c 10) ≡≡ u x • (c 14). ( 20
)
3. In the third iteration, rewriting the (imp-li) gives

(lpi b f) • f id 1 • pbl • (t ? <)• l x , (c 11) • u x • (c 10) ≡≡ u x • (c 14). (21)
As in step 2, the looping pre-condition evaluates into (c true) forcing us to reiterate the above procedure, given in the step 1, which results in

We rewrite the Lemma 7.2, and get

(lpi b f) • f id 1 • in 2 • u x • (c 14) ≡≡ u x • (c 14). (26)
Now we rewrite (s_lcopair_eq) and handle

id 1 • u x • (c 14) ≡≡ u x • (c 14) (27)
which is trivial, since the identity term disappears when to compose and the equality sort ≡≡ is reflexive.

Lemma 7.11. For each x y : Loc, e : EName, if program pieces prog5 and prog6 are given as in the following listings, then dCmd (prog5) ≡≡ dCmd (prog6). Proof: In the proof structure, we first tackle with the downcast operator. The second task is to deal with the first loop iteration which has the state but no exception effect. In the third, we study the second iteration of the loop where an exception is thrown which is followed by the abrupt loop termination. Finally, in the fourth step, we explain the exception recovery and the program termination. Below is the sketch of prog5:

1 in 1 tag e G G O [ ] 1
) ) ≤ 0) then (THROW e) else (x x -1)), c 2 = (x x -1), c 3 = (y 7). The dotted arrows depict the normal loop iterations while dashed ones are to identify the program behavior after the exception of name e is raised. Using the rules of the logic L st+exc , we can reduce the above diagram into the one given below with respect to the equality sort ≡≡:

1 in 1 b G G B pbl G G 1 + 1 [ ] 1 •tag e c 2 G G 1 lpi (c true) c 1 lpi (c true) c 1 1 in 2 y y c 2 U U 1 in 1 id 1 9 9 1 c 0 G G 1 pbl • (c true) G G 1 + 1 (lpi (c true) c 1 )• [ ] 1 •tag e c 2 •pbl•b id 1 G G 1 in 1 G G 1 + O id 1 c 3 • untag e G G 1 1 in 2 y y id 1 Q Q O in 2 y y untag e G G 1
1 c 0 G G Z u x G G 1 c 7 G G Z u y G G 1
which is actually the prog6 when sketched.

Automating decorated proofs

A rule in a decorated logic only applies if the given term gets decorated as expected by the rule. Therefore, decoration checks are pretty important and occur pretty often. To automatize this checks, at the Coq level, we already have tactics decorate and edecorate. See them here (xvii) . Also, we plan to put [START_REF] Czajka | Hammer for Coq: Automation for dependent type theory[END_REF]'s CoqHammer tool in use to try automatizing such program property proofs, done within the scope of decorated logics, implemented in Coq.

On the completeness of the logic L st+exc

With the logic L st+exc , no generic program properties such as dCmd(p 1 ) ≡≡ dCmd(p 2 ) =⇒ ∀ s s , eval p 1 s s =⇒ eval p 2 s s can be proven. Here, eval denotes the big-step semantics of the commands until reaching SKIP. Only programs that admit a particular specification can be proven to be equivalent with respect to the state and exception effects. The total correctness is based on a syntactic completeness property. In a way, it is meant to make sure that we are not using too many axioms to construct a denotational semantics for the IMP+Exc language using the logic L st+exc as the target language. This syntactic completeness property is called relative Hilbert-Post Completeness (rHPC) and elaborately defined by [START_REF] Dumas | Relative hilbert-post completeness for exceptions[END_REF]. Briefly, given two logics L 0 and L such that L 0 ⊆ L (L 0 is a sub-logic of L) and a theory T of L. T is relatively Hilbert-Post complete with respect to L 0 if (1) at least one sentence is unprovable in T (not the maximal theory ensuring consistency), and (2) every theory containing T can be generated from T and some sentences from L 0 . Here, L 0 can be seen as the pure logic that governs the denotational semantics of the effect-free subset of the IMP language where L is the logic that governs the denotational semantics of the superset of the IMP language after either the state or exception effect is added. We prove, in Theorem 6.8.5 in [START_REF] Ekici | Certification de programmes avec des effets calculatoires[END_REF]), that the decorated theory of exceptions is relatively Hilbert-Post complete with respect to its pure part. However, only the core part of the decorated logic for the state effect is proven to be rHPC (see Theorem 5.4.9 in [START_REF] Ekici | Certification de programmes avec des effets calculatoires[END_REF]). What we mean by the "core part" is the logic with no categorical pairs. Clearly, when translated to IMP denotational semantics, it corresponds to the part that governs conditionals and loops. We can conjecture that the logic is still complete in the presence of categorical pairs. However, the proof is not yet done.

In the rHPC proof of the core part for the decorated logic for the state, we first determine the canonical forms of accessors and modifiers and then show that both such forms are equivalent to some finite set of equations in the pure sublogic of L st with no pairs. In the presence of categorical pairs, we so far had difficulties to come up with the canonical forms for accessors and modifiers even though it is clear that such forms exist. Once we have these forms in hand, it should also be the case that the rules governing pairs suffice to prove that such forms are equivalent to finite number of equations made of terms coming from the pure counterpart of the logic L st . We plan to study this in the near future.

It is also proven that if two theories are rHPC with respect to a (pure) logic, then the combination of these theories remains to be rHPC. Therefore, the logic L st+exc without the use of pairs is rHPC.

  Figure 1: The approach

Figure 3 :

 3 Figure 3: Big-step operational semantics for arithmetic expressions

Figure 4 :

 4 Figure 4: Big-step operational semantics for Boolean expressions

Figure 5 :

 5 Figure 5: Small-step operational semantics for commands

Figure 6 :

 6 Figure 6: Syntax for exceptional commands

Figure 7 :

 7 Figure 7: Small-step operational semantics for additional commands

Figure 8 :

 8 Figure 8: L meq : syntax

Figure 9 :

 9 Figure 9: L meq : rules

Figure 10 :

 10 Figure 10: L dec : syntax

Y

  (2) : X → Y as a function c : X+E → Y+E. The complete and detailed category theoretical model is given in(Ekici, 2015, §6.1).Definition 5.1. For each type Y and exception name e, the propagator throw • tag(1) e : EV e → Y Intuitively, raising an exception of name e is first tagging the given ordinary value with e and then coercing the empty type into Y for the continuation issues.

( 6 )

 6 d Try 0 . Pure code inside try never triggers the code inside catch. ∀ e ∈ EName, u (0) : X → Y, b (1) : EV e → Y, try(u)catch(e ⇒ b) (1) ≡ u (0) : X → Y. (7) d Try 1 . The code inside catch is executed as soon as an exception is thrown inside try. ∀ e ∈ EName, u (0) : X → EV e , b (1) : EV e → Y, try(throw e • u)catch(e ⇒ b) (1) ≡ b (1) • u (0) : X → Y.

2 :

 2 Definition throw (X: Type) (e: EName) (@empty X) o tag e. Definition try_catch (X Y: Type) (e: EName) (f: term Y X) (g: term Y (Val e)) downcast (copair (@id Y) (g o untag e) o in1 o f).

Figure 17 :

 17 Figure 17: L st+exc : rules

  pbl:= tpure (bool_to_two).where bool_to_two (b : bool) := (if b then (inl void) else (inr void)).

Figure 18 ::

 18 Figure 18: Additional rules on pure terms: IMP+Exc specific

Figure 19 :

 19 Figure 19: (cond b c 1 c 2 ) and (while b do c) in L st+exc

Figure 20 :

 20 Figure 20: (THROW e) and (TRY c 1 CATCH e ⇒ c 2 ) in L st+exc

Fixpoint

  dCmd (c: Cmd): (term unit unit) match c with | skip ⇒ (@id unit) | sequence c0 c1 ⇒ (dCmd c1) o (dCmd c0) | assign j e0 ⇒ (update j) o (daExp e0) | cond b c2 c3 ⇒ copair (dCmd c2) (dCmd c3) o (pbl o (dbExp b)) | while b c4 ⇒ (copair (lpi (pbl o (dbExp b)) (dCmd c4) o (dCmd c4)) (@id unit)) o (pbl o (dbExp b)) | THROW e ⇒ (throw unit e) | TRY_CATCH e c1 c2 ⇒ (try_catch e (dCmd c1) (dCmd c2)) end.

(

  lpi b f) • u x • (c 14) ≡≡ u x • (c 14). (22)4. In the fourth step, rewriting the (imp-li) gives(lpi b f) • f id 1 • pbl • (t ? <)• l x , (c 11) • u x • (c 14) ≡≡ u x • (c 14). (23)By rewriting commutation -lookup -constant -update, we obtain(lpi b f) • f id 1 • pbl • (t ? <)• (c 14), (c 11) • u x • (c 14) ≡≡ u x • (c 14). (24)Finally here, the looping pre-condition (t ? <)• (c 14), (c 11) evaluates into (c f alse) yielding(lpi b f) • f id 1 • pbl • (c f alse) • u x • (c 14) ≡≡ u x • (c 14).

  , c 0 = (x 1; y 20), c 1 = (if (x ?

  1. Initially, we have↓ id 1 c 3 •untag e •in 1 • (lpi (c true) c 1 )• [ ] 1 •tag e c 2 •pbl•b id 1 •pbl•(c true) • u y • (c 20) • u x • (c 1) ≡≡ u y • (c 7) • u x • (c 0). (28)We convert ≡≡ into ≡∼, then rewrite the (w_downcast) rule and getid 1 c 3 • untag e • in 1 • (lpi (c true) c 1 ) • [ ] 1 • tag e c 2 • pbl • b id 1 • pbl • (c true) • u y • (c 20) • u x • (c 1) ≡∼ u y • (c 7) • u x • (c 0). (29)Rewriting commutation-update-update, on both sides, givesid 1 c 3 • untag e •in 1 • (lpi (c true) c 1 ) • [ ] 1 • tag e c 2 • pbl • b id 1 • pbl • (c true) • u x • (c 1) • u y • (c 20) ≡∼ u x • (c 0) • u y • (c 7). (30) Rewriting Lemma 7.3 yields id 1 c 3 • untag e •in 1 • (lpi (c true) c 1 ) • [ ] 1 • tag e c 2 • pbl • b id 1 • in 1 • u x • (c 1) • u y (c 20) ≡∼ u x • (c 0) • u y • (c 7). (31)2. Now we rewrite the rule (w_lcopair_eq), and handleid 1 c 3 • untag e • in 1 • (lpi (c true) c 1 ) • [ ] 1 • tag e c 2 • pbl • b • u x • (c 1) • u y • (c 20) ≡∼ u x • (c 0). (32)By unfolding b, we haveid 1 c 3 • untag e • in 1 • (lpi (c true) c 1 ) • [ ] 1 • tag e c 2 • pbl • (t ? ≤) • l x (c 0) • u x • (c 1) • u y • (c 20) ≡∼ u x • (c 0) • u y • (c 7).(33)By rewriting the lemma commutation-lookup-constant-update, we obtainid 1 c 3 • untag e •in 1 •(lpi (c true) c 1 ) • [ ] 1 • tag e c 2 • pbl • (t ? ≤) • (c 1), (c 0) • u x • (c 1) • u y • (c 20) ≡∼ u x • (c 0) • u y • (c 7). (34)We rewrite the rule (imp 2 ), and get id 1 c 3 • untag e • in 1 • (lpi (c true) c 1 ) • [ ] 1 • tag e c 2 • pbl • (c false) • u x • (c 1) • u y • (c 20) ≡∼ u x • (c 0) • u y . • (c 7). (35)

  If f does not throw any exception then no handling is performed, we have id term in execution. Note also that the term in 1 Y,O used in the Definition 5.2 is the horizontal one in the above diagram, and implicitly means that Y and Y + O isomorphic objects. The inclusions in 1 Y,O (the vertical in the above diagram) and in 2 Y,O play a role in the equational reasoning, given in Figure

  . Remark 7.1. An expression in in IMP+Exc can have memory access right (i.e., a variable x) but can never throw or catch exceptions. To calculate the decoration d of an arithmetic expression pair, i.e., daExp a 1 , daExp a 2

	(d,0) l	, we use the following strategy:

(xvii) https://github.com/ekiciburak/impex-on-decorated-logic/blob/master/Decorations.v

Acknowledgements

We wish to thank the two anonymous reviewers for their careful reading of our manuscript and for insightful comments and suggestions. We thank Jean-Guillaume Dumas and Dominique Duval for their support on all aspects of the presented logics. Many thanks also to Damien Pous for his guidance on Coq related questions. This work has been partially supported by the Austrian Science Fund (FWF) grant P26201 and the European Research Council (ERC) Grant No. 714034 SMART.

Burak Ekici

Now, we cut t (λ x : unit.bool_to_two false) ≡≡ in 2 (4)

and rewrite it back in the goal. So that we obtain

(5)

Then, we use (s_lcopair_eq), and finally have g ≡≡ g which is trivial since ≡≡ is reflexive. It remains to show that the cut statement in Equation 4 holds. By simplifying t (λ x : unit. bool _to _two false) and unfolding in 2 , we have t (λ x : unit.inr x) ≡≡ t (inr).

Now, we apply (imp 6 ) and get ∀x : unit, inr x =inr x (7)

which is trivial since the Leibniz equality '=' is reflexive. If b = true, by following above procedure with true (instead of false) we first handle

and then freely convert ≡≡ into ≡∼. There, rewriting the rule (w_lcopair_eq) yields f ≡∼ k. We unfold k with b = true and get

Now by rewriting (w_lcopair_eq), we have f ≡∼ f. This is again trivial, since the equality sort ≡∼ is reflexive.

Lemma 7.10. For all x : Loc, if program pieces prog3 and prog4 are given as in the following listings, then dCmd (prog3) ≡≡ dCmd (prog4). Proof: In the proof structure we intend to reduce prog3, first dealing with the pre-loop assignments and the looping pre-condition. Since it evaluates into true, in the second step we identify things related to the first loop iteration. The third step primarily studies the second and then the third loop iteration after which the looping pre-condition switches to false. Finally, we explain the program termination and show that prog3 does exactly the same state manipulation with prog4. Note also that we do not need to check the results they returned, since all IMP+Exc commands, thus programs, return void : U.

Below is the sketch of prog3:

Using the rules of the logic L st+exc , we simplify this diagram into the one given below with respect to the equality sort ≡≡:

which is actually prog4 when sketched.

1. Initially, we have

Let us simplify it as far as possible. By rewriting commutationlookupconstantupdate (see Figure 21), we obtain

Since the looping pre-condition (t ? <) • (c 2), (c 11) evaluates into (c true), and due to (imp 3 ), we have

By rewriting the Lemma 7.3, we get

Here, we first convert ≡≡ into ≡∼ then rewrite (w_lcopair_eq), and end up with

in which the second appearance of f unfolds into

Rewriting the Lemma 7.2 yields

We now rewrite (s_lcopair_eq) which gives

Here, by unfolding c 2 , we have

Rewriting the lemma commutationlookupconstantupdate gives

We rewrite (imp 1 ), and get

We again rewrite the lemma commutation-update-update, and obtain

3. We re-iterate the loop via (imp-li), and have

We rewrite Lemma 7.3, (w_lcopair_eq), then unfold c 1 , and get:

By rewriting commutationlookupconstantupdate, (imp 3 ) and Lemma 7.3, we have

By (w_lcopair_eq), the exception is raised:

Due to the raised exception, the infinite loop gets abruptly terminated at this step. Here we unfold the definition of THROW then rewrite propagator-propagates (see Section 6.1), and get

4. Here, we first cut in 1 • [ ] 1 ≡≡ in 2 , and rewrite it back in the equation. Thus, we have

By rewriting (s_lcopair_eq), we obtain

Since

) is pure with respect to the exception, we rewrite (eax 1 ), and get

Unfolding the definition of the command c 3 = (u y • (c 7)), we have

We now rewrite commutation-update-update on the left, and handle

Finally, it suffices to rewrite interaction-update-update,

which is trivial since the equality symbol ≡∼ is reflexive. However, it still remains to prove the previous cut in 1 • [ ] 1 ≡≡ in 2 : since everything is pure with respect to the exception, we have

Now, rewriting the rule (w_empty) gives [ ] 1+1 ≡∼ [ ] 1+1 . This is trivial since the equality sort ≡∼ is reflexive.

The full Coq proofs of above lemmata can be found here (xv) , and the entire implementation there (xvi) .

(xv) https://github.com/ekiciburak/impex-on-decorated-logic/blob/master/IMPEX_Proofs.v xvi) https://github.com/ekiciburak/impex-on-decorated-logic

Concluding remarks

We have presented frameworks for formalizing the treatment of the state and the exception effects, first separately, and then combined, using the decorated logic. Decorations describe what computational effect evaluation of a term may involve, and form a bridge between the syntax and its interpretation in reasoning about terms by making computational effects explicit in the decorated syntax. We have designed a denotational semantics for the IMP+Exc language over the combined decorated logic L st+exc . This way, we managed prove some strong equalities between IMP+Exc programs. We have also encoded the combined logic in the Coq proof assistant and certified related proofs.