G. Winskel. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993. 75  @ NUS  Home/Search   Document Not in Database   Summary   Related Articles   Check

....the calling relation, called there the recursion relation can be e#ectively used. The program terminates if and only if the calling relation is wellfounded. Thus, the condition expressed by Definition 1 is necessary for termination. The main theorem behind wellfounded recursive definitions ([16], Theorem 10.19) as proved in HOL by Nipkow, reads as follows: Theorem 1 ( 13] Let F : A B) and let # be a wellfounded relation on A. Let # = wfrec # F . Then for every x A. # We do not need to know the exact definition of the function wfrec. Its existence is the point of the ....

G. Winskel. The Formal Semantics of Programming Languages: an Introduction. MIT Press, 1993. 22

....advantages in endowing a programming language with a good denotational semantics. First of all, the denotational semantics is typically better suited than the operational one for comparing di erent languages and or di erent programs, since it naturally abstracts from di erences in the syntax [Win93] This is especially true for a language such as tcc whose operational semantics is given by three di erent transition systems. In comparison, the denotational semantics is obtained by a standard xpoint computation over a cpo. This also simpli es the goal of proving program properties by static ....

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing Series. The MIT Press, 1993.

....M has type #. Note that x need not be a function only, we might define recursive values this way as well. For instance, we have (using Haskell like notation) let ones = 1 : ones in ones fix (#ones. 1 : ones) The least fixed point theorem states that fix f is the least fixed point of f [76, 92]. That is, i) it satisfies the fixed point property: f (fix f) fix f , and (ii) it is the least such value, i.e. for all x s.t. x = f x, we have fix f x. We use the name fix only to mean this particular fixed point operator over domains. The theory of fixed points is extensively studied ....

....The Bekic property of fix states that: fix (#x. fix (#y. f (x , y) fix (#x. f (x , x ) Or, equivalently, fix (#t. fix (#v. f (# 1 t , # 2 v) fix f where f : # # # #. It is easy to generalize to arbitrary number of variables, rather than just two; see Winskel s textbook for details [92]. In Chapter 6, we consider fixed point operators in more abstract settings, i.e. without assuming that the underlying structure is domains and continuous maps. We assume a minimal acquaintance with category theory in the following discussion [2, 70] The basic structure we work with is a ....

Winskel, G. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing series. MIT Press, Feb. 1993. (140, 141)

....[ f] as the least xed point of an operator mapping partial functions to partial functions. p m q p q) p 1 p m q p q) The de nition of F is standard, and we refer the reader to any book on semantics of functional programming languages for its details (for example, Win93] For the mutual recursive de nition of the functions f 1 , f n , the associated operator maps n tuples of partial functions to n tuples of partial functions, q p n q) p 11 q p n q) and the partial function denoted by [ f i ] is ....

....type theory. In [Nor88] Nordstr om uses the predicate Acc for that purpose. One can adopt a set theoretic approach and see functions as relations. Specifically, the behaviour of a recursive function can be described by an inductive relation giving its operational semantics (see, for example, Win93] Operational semantics has been developed in type theory in [BCB02] and [ZMHH02] However, relations do not have any computational content in type theory. The real challenge consists in representing general recursive programs as elements of some functional type. Using classical logic it is ....

G. Winskel. The formal semantics of programming languages: an introduction. The MIT Press, 1993.

....lens. We write this lens l . Let l 0 . be an increasing chain of (very )well behaved lenses, by lemma 3.3.4 there exists a least upper bound of this chain that is a (very) well behaved lens. # We will make use of the following standard theorem from domain theory (c.f. [33]) Recall that a function f between two cpos is continuous if it is monotonic and if for all increasing chains we have f( n#w l n ) n## f(l n ) A fixed point fix (f) is such that fix (f) f(fix(f ) 3.3.7 Theorem [Fixed Point Theorem] Let f be a continuous function from D to D where D ....

....f (# l ) Then fix (f) is a fixed point of f and the least prefixed point of f . 8 Theorem 3.3.6 tells us that we can apply Theorem 3.3.7 to continuous functions from lenses to lenses to define recursive lenses. More generally, we can apply standard domain theory (as described, for example, in [33]) to interpret a variety of constructs for defining continuous lens combinators. We say that an expression e is continuous in the variable x if the function #x.e is continuous. An expression in continuous in its variables, or simply continuous, if it is continuous in every variable. Examples of ....

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993. 32

....smaller than every other element. In our setting, l is the lens whose put and get function are undefined everywhere. 3.3.1 Theorem: Let L be the set of well behaved lenses between C and A.Then(L, is a cpo with bottom. We can now apply standard domain theory (as described, for example, in [31]) to interpret a variety of constructs for defining continuous lens combinators. In particular, every continuous function on well behaved lenses has a least fixed point that is a well behaved lens. 4. TRANSFORMING TREES We now describe our surface language, Hocus Focus. We first formally define ....

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993.

....is deterministic if no define define dependence is present between any two different body instances of the forall statement. We want to record the concept of the forall statement in a semantic model, such that we can use this model to reason about a program. We use denotational semantics [1] [16], in which the meaning of a program can be expressed by the composition of the meanings of its parts. The denotational semantics are useful when we want to rewrite only parts of a program, and leave the meaning of the whole program as it is. In denotational semantics a program state captures all ....

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. Foundations of Comp. Series. MIT Press, 1993.

....the transduction. 3 Interactive relations and programs Given a sequence u 2 f0; 1g and t 0, let pref t (u) be the length t pre x of u. For nite or in nite strings u we write x y if x is a nite (and strict) pre x of u. We paraphrase the common de nition of monotonic functions (cf. [34]) for the case of partial functions as follows. De nition 4. A partial function g : f0; 1g is called monotonic if for all x; y 2 f0; 1g , if x y and g(y) is de ned then g(x) is de ned as well and g(x) g(y) The following observation captures some aspects of the computational model ....

....the output generated so far and vice versa, without retraction of any earlier output signals. Interactively computable functions clearly all have this property on de ned values, which can be more precisely formulated as follows. We paraphrase the classical de nition of continuous functions (cf. [34]) for the case of functions on in nite strings. is called limit continuous if there exists a classically computable partial function g : f0; 1g such that the following conditions are satis ed: 1) g is monotonic, and (2) for all strictly increasing chains u 1 u 2 u t : ....

G. Winskel. The formal semantics of programming languages: an introduction, The MIT Press, Cambridge (Mass.), 1993.

....we de ne the operational semantics of our extended logic language. We choose a syntax directed style of presentation which makes use of deduction rules. For an elementary presentation of this technique sometimes called structural operational semantics or natural semantics, the reader may refer to [22]. Before de ning the semantics of our logic language, we recall the following notions. By fV 1 =u 1 ; Vm=umg we denote the substitution of the arguments u 1 ; um for the variables V 1 ; Vm (as usual, we assume that the V i s are all distinct and for i = 1; m, u i ....

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. The MIT Press, 1993. 37

....With this background it was possible, for the first time, to consider categorical models for a rich type theory with recursive types. In [Fio94a, FP94] a notion of categorical model for the metalanguage FPC a type theory with sums, products, exponentials and recursive types [Plo85, Gun92, Win93] was defined. Very roughly, categorical models of FPC are algebraically compact partial cartesian closed categories with binary coproducts. Impact of axiomatic domain theory In relating operational and denotational semantics. The investigation of the relation between operational and ....

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. The MIT Press, 1993.

....semantics is still too complex even if restricted to the relevant language fragment; this is mostly due to the fact that SML contains imperative constructs which are out of the scope of this paper. Instead, we use the more vanilla operational semantics of an eager language following closely [22]. We consider the task of bridging the gap between Real SML in the sense of [14] and our language which we call AbstractSML as routine. 3.1 Expressions of AbstractSMl The key ingredient of this operational semantics is an inductively defined subset of all terms, the so called set of ....

....5.2 The instance FIX The language WF, constrained to total functions, had to rule out values like hd [ or 3 div 0. When admitting partial functions, there is the well known choice for the semantics of function application reflecting call by value evaluation or call by name evaluation (cf. [22]) An appropriate semantical framework for tackling these issues is denotational semantics, which we use as basis for our second program notion FIX. There are many known formalisations of denotational semantics in HOL systems. For Isabelle HOL, there is most notably HOLCF [17] Instead, we will ....

[Article contains additional citation context not shown here]

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993.

....side) replaced by Fr i , and then define Fr P = # i Fr i P . Roughly said, the least solution may be computed by taking Fr X to be within the body and Fr(body X ) elsewhere . All this can be formalised and proved by standard fixed point theory, as explained, for instance, by Winskel [10]. The same remark applies to the coming definitions of the set valued functions # (9) and # (11) Skip this remark about Syntax. An expression that has no free variables is called closed. As a syntactic constraint, we require that the entire, root, process is closed. For example, in the ....

....so that the definition of # reads: # = B#. As remarked at the definition of Fr in 8, the least fixed point of the equation # = B# equals # i # i , where # 0 = #P . and # i 1 = B# i . For such a function, the following fixed point induction principle holds (consult for example Winskel [10] for the underlying theory) Suppose ( Base ) property P holds of function # : #P . and suppose ( Step ) # # . P(#) # P(B#) Then ( Conclusion ) P holds of # : # i # i . This is only true of admissible predicates P . Equality of functions is admissible. The principle generalises ....

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing series. MIT Press, Cambridge MA, 1993. 20

....it may not change or reduce the amount of data it has already produced, nor may it wait forever. By requiring all processes to use such blocking reads, Kahn s systems are provably deterministic. There is much more to denotational semantics. See one of the introductory textbooks by Winskel [73], Gunter [29] Stoy [65] Schmidt [60] and Allison [1] 3.1.2 Circuit Simulation Circuit simulation has traditionally proceeded along two paths. Analog simulation attempts to model virtually all circuits, whereas digi35 Chapter 3 Semantics In Out In Out 0 1 1 0 B A (a) b) c) Figure 3.2 ....

....fixed point, in which case the element is unchanged. 39 Chapter 3 Semantics Davey and Priestley s textbook on order in mathematics [23] is perhaps the best general introduction to this subject. The programming language semantics community is the other main source. I recommend the books by Winskel [73] (my primary source of notation) and Gunter [29] Others include Allison [1] the very readable unpublished manuscript by Turbak, Gifford, and Reistad [70] and chapters in the second volume of the Handbook of Theoretical Computer Science [71] 3.2.1 Complete Partial Orders Definition 1 A ....

[Article contains additional citation context not shown here]

G. Winskel. (35, 39, 69, 77) The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing. MIT Press, 1993.

....solutions for Fr that satisfy the equations for Fr . To fix just one particular solution, we stipulate that, for any P , the set Fr P is least with respect to set inclusion. For the semantics of recursion, the reader may consult standard fixed point theory, as explained, for instance, by Winskel [10]. 9 Saturation of events. An expression is called saturated if it has no occurrences of variables, neither x nor x . So, a saturated expression is closed. Here we define the saturation # that transforms events to saturated events, in an environment #; later on we deal with processes (16) In ....

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing series. MIT Press, Cambridge MA, 1993. 15

....state paths) and precludes further interleaving. The semantics of ULTRA, which is based on increments rather than on states is compact and easy to understand. Additionally, it is compositional and thus well suited for verification by formal means, e.g. using an extended version of Hoare s logic [Win93] developed for the verification of sequential programs. The open semantics of Concurrent Transaction Logic can also be used for formal verifications, but the overall meaning of a formula is more complicated than in the ULTRA context, as it has to take arbitrary interleaving with non specified ....

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993.

....is. In this way, we consider that the operations form a somewhat minimal set of primitives for computing. However, instead of presenting exhaustively the whole minimal set, we consider that (mathematical) computation has been exploited and, because of this, we avoid reproducing literature (e.g. [31, 40, 48, 49, 56, 63, 64]) which provides a minimal imperative language, typically with while statement and so on. Thus, we formalize the operational semantics that complement theirs and give a few local primitives. Thus our working objects are: Real constants. The space initialization. The create statement, ....

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing. The MIT Press, 1997.

....is. In this way, we consider that the operations form a somewhat minimal set of primitives for computing. However, instead of presenting exhaustively the whole minimal set, we consider that (mathematical) computation has been exploited and, because of this, we avoid reproducing literature (e.g. [31, 40, 48, 49, 56, 63, 64]) which provides a minimal imperative language, typically with while statement and so on. Thus, we formalize the operational semantics that complement theirs and give a few local primitives. Thus our working objects are: Real constants. The space initialization. The create statement, ....

G. Winskel. The Formal Semantics of Programming Languages: an introduction. The MIT Press, fourth edition, 1997.

....R D Wlp pH R # D # Wp # gH # # # # # R # angelic natural demonic infinite Hoare s axiomatic Dijkstra s pred trans Denotational Relational Trace based Figure 1: Semantics in Cousot s hierarchy. 4. PROGRAM MANIPULATION In the following we consider a simple imperative language, Imp [33], with the following syntax: c : nil id : e c; c if e then c else c while e do c We know that the denotational semantics is compositional , namely it is equal to the composition of the semantics of program s sub components. We want to give a characterization of this property ....

....] A and [ P 2 ] A in order to obtain [ P ] A , since we have lost the history of the computation of the programs above. Another problem related with equation (Comp) corresponds to characterize how the semantics # behaves in presence of divergence. It is known that in standard semantics [33], if the X component diverges then #(X # Y ) #(X) Even if equation (Comp) holds, this fact represents a bound in compositionality because for any two computations Y #= Z, if X diverges then #(X # Y ) #(X) #(X # Z) In this case we are unable to characterize what may happen beyond ....

Winskel, G. The formal semantics of programming languages: an introduction. MIT press, 1993.

....works embed CCS and the # calculus in various proof tools. 7. 1 Formal Semantics for Concurrent Programming Languages By now it is a straightforward activity to equip a programming language with some kind of formal semantics, and numerous textbooks are available on the topic, e.g. Winskel [Win93] and Nielson [NN92] In this section we will briefly recall some efforts to provide formal semantics for languages that are comparable to ERLANG in the sense that they offer a notion of concurrency and support message passing. Further their primary use is as programming languages rather than for ....

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. The MIT Press, Cambridge, MA, 1993.

....is deterministic if no define define dependence is present between any two different body instances of the forall statement. We want to record the concept of the forall statement in a semantic model, such that we can use this model to reason about a program. We use denotational semantics [1] [13], in which the meaning of a program can be expressed by the composition of the meanings of its parts. The denotational semantics are useful when we want to rewrite only parts of a program, and leave the meaning of the whole program as it is. In denotational semantics a program state captures all ....

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing Series. MIT Press, 1993. 11

....A n ### . This is done in order to distinguish the everywhere undefined function from the undefined object of type # # #. The structures A v # were first defined in the dissertation of Platek [21] Platek called them HC functionals. The structures A n # are used in denotational semantics [10, 30]. 5.1 Interpretation of programs as partial functions Programs t of type # can be interpreted with respect to variable assignments as points in the space A v # in a canonical way. An assignment # in A is a function that assigns to every variable x of type # an object #(x) of A v # . ....

....n A #= # # i# eval n A (t) is defined. Let t # be a closed term of basic type and a # A # . Then we have: 6.3) t] v A = a i# eval v A (t) c a . 6.4) t] n A = a i# eval n A (t) c a . These four facts are well known. Proofs can be found, for example, in Winskel s book [30]. Since we use these results in Sect. 8 and Sect. 9 to show that the logics VPT and NPT are adequate for strict and non strict evaluation, we sketch the proofs here briefly. 14 6.1 Strict evaluation and the structures A v # One direction is easy. If eval v A (t) v, i.e. if t # ev v v ....

G. Winskel. The Formal Semantics of Programming Languages: an Introduction. The MIT Press, 1993. 36

....for tool development. It is also necessary to de ne the meaning of the concepts, the semantics. In computing, language de nition generally focuses on the meaning of textual programming languages. Semantics may be expressed in denotational, operational, axiomatic or algebraic ways (amongst others)[9]. A denotational approach is well adapted to the expression of the semantics of a graphical notation, since it de nes the symbolic representations of things, the meaning of the things denoted, and a mapping between the two. 2.1 Issues in Language De nition for UML There are a number of current ....

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing. MIT Press, Cambridge Mass., 1993.

....e ] # #, ##=#v ## ,# ## ##(v # = v ## ) # (# = # ## ) ##, #, ss## ss ## # ,# # ,ss # ####,#, ss## ss ## ## ,# ## , ss # # # (# # = # ## ) # (# # = # ## ) STRUCTURAL OPERATIONAL SEMANTICS 85 Given Theorem 4. 1, this result follows from the theory of sequential programs [9, 21]. # Theorem 5.3. The statement wait on # for # until true; causes the enclosing process to suspend forever. Proof: We need to show that ##, #, #, ws i [#, true] ss## # pgm ##, #, #, ws i [#, true] ss# This is a consequence of the definition of run predicate used in defining the ....

....for sx from x1 and x2 respectively. The above program is portable if and only if the value written into sx by the two processes is identical in every cycle. That is, Func1 and Func2 stand for the same function. However, since the equivalence problem for Turing complete languages is undecidable [21], the portability cannot be tested algorithmically. # In order to detect lack of portability of a VHDL 93 description at run time, the simulator can be augmented with additional information specified in the DFA described in Sections 4.1.1 and 4.1.2. One can view this information as a new ....

G. Winskel, The Formal Semantics of Programming Languages: An Introduction, The MIT Press, Cambridge, MA 1993.

....bop over boolean connectives, and rop over relational operators. x ranges over identifiers. We assume all identifiers have a given typing. Identifiers which are not introduced locally are defined by a global declaration. This is an explicitly typed, higher order variation of the language REC in [70], extended with data field primitives. The typing rules for the extensions are straightforward and we omit them here. The data field free part of the language can be given a denotational semantics in a standard way, as a function mapping from terms and identifier binding environments to elements ....

....type for data fields, and the definitions could thus be reused for any kind of data field. 10 4 Preliminaries 4.1 A Metalanguage for Partial Functions We now define a small metalanguage for partial functions. Essentially this is a variation of the metalanguage for continuous functions in [70]. Since we want to be able to embed our concepts into various host languages we do not specify all the details of the language completely; rather, we give a language scheme. We consider the following kind of cpo s: ffl Basic cpo s which are flat cpo s denoted by constant symbols, in particular ....

[Article contains additional citation context not shown here]

G. Winskel. The Formal Semantics of Programming Languages -- An Introduction. MIT Press, 1993.

....) g[g 1 ] the local variables of g 1 in c are those in the set vars(g 1 ) fV 1 ; Vm g [ vars(g[ 6. 3. Operational semantics In this section we de ne a big step operational semantics for our logic language (for an elementary presentation of this technique the reader may refer to [20]) Given a program P , we de ne the semantics of P as a (possibly empty) ternary relation P g 7 b, where g is a goal and b is either true or false, denoting that for P and g all the LD derivations are nite, and either one of them is successful, in which case b is true, or all of them are ....

G. Winskel, The Formal Semantics of Programming Languages: An Introduction. The MIT Press, 1993.

....0 i E [ e i ] hoe; i = hv 00 ; 00 i ) v 0 = v 00 ) 0 = 00 ) hoe; ss i ss hoe 0 ; 0 ; ss 0 i hoe; ss i ss hoe 00 ; 00 ; ss 0 i ) oe 0 = oe 00 ) 0 = 00 ) Given Theorem 4. 1, this result follows from the theory of sequential programs [9, 21]. Theorem 5.3 The statement wait on ; for 1 until true; causes the enclosing process to suspend forever. Proof: We need to show that hoe; ws i [1; true] ssi pgm hoe; ws i [1; true] ssi This is a consequence of the definition of run predicate used in defining the semantics of ....

....for sx from x1 and x2 respectively. The above program is portable if and only if the value written into sx by the two processes is identical in every cycle. That is, Func1 and Func2 stand for the same function. However, since the equivalence problem for Turing complete languages is undecidable [21], the portability cannot be tested algorithmically. In order to detect lack of portability of a VHDL 93 description at run time, the simulator can be augmented with additional information specified in the DFA described in Sections 4.1.1 and 4.1.2. One can view this information as a new ....

Winskel, G., The Formal Semantics of Programming Languages: An Introduction, The MIT Press, 1993. 25

....structures as functions with non contiguous, possibly non numerical domains. Calls to a function outside its domain return an error value , with algebraic properties similar to the divergent element . We define partial functions in a variation of the metalanguage for continuous functions in [23], extended with the constant . Within this language, we can now define most types of collection oriented operations [20] as higher order functions operating on partial functions [7, 14] The language, however, lacks operations which extract the domain of a function or any information pertaining to ....

....the case when f and g are recursively defined, say we have a simultaneous recursive definition (f; g) F (f; g) where F is a continuous function. The condition on f and g in Definition 1 is an inclusive (or admissible) predicate, which means we can use Scott s fixed point induction to prove it [23]. Proposition 1. Define (f ; g ) as the least fixed point to (f; g) F (f; g) and let (f 0 ; g 0 ) f i ; g i ) F (f i Gamma1 ; g i Gamma1 ) for i 0. Then f is implemented by g under (OE 0 ; OE 1 ) if 8i 0: 8x: f i Gamma1 (x) g i Gamma1 (OE 0 x) OE 1 x) 8x: f i (x) g ....

G. Winskel. The Formal Semantics of Programming Languages -- An Introduction. MIT Press, 1993.

....the di erent programming languages. A methodology which is often used for de ning the semantics of programming languages, is based on the concept of inductive de nitions presented by means of rule sets (see, for instance, 1] for a survey of some theoretical results on inductive de nitions, and [16] for their application to the de nition of the operational semantics of some imperative, functional, and concurrent programming languages) A rule is pair of the form (X=y) also written as X y , where X is a set of premises and y is a conclusion. For instance, in the case of a simple ....

.... (v) function declarations, we may de ne the operational semantics of call by value by the in nite set R of rules which are derived, as we will indicate below, from the following ve schematic rules (here and in what follows we feel free to omit the curly brackets when writing a set of premises) [16]: r1) n n (r2) t 1 n 1 t 2 n 2 t 1 op t 2 n if n = n 1 op n 2 ) r3) t 0 0 t 1 n 1 if t 0 then t 1 else t 2 n 1 (r4) t 0 n 0 t 2 n 2 if t 0 then t 1 else t 2 n 2 if n 0 6= 0 (r5) t 1 n 1 : t k n k d[n 1 =x 1 ; n k =x k ] n f(t 1 ; t k ) ....

[Article contains additional citation context not shown here]

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. The MIT Press, 1993.

....model this behaviour, we de ne our operational semantics as a ternary relation P : G 7 , where is either a substitution or false. This relation is de ned inductively by the following rules. For an introduction to the theory of inductively de ned operational semantics the reader may refer to [154]. In these rules, i) the composition of two substitutions and [103] is denoted by , ii) denotes the empty substitution (that is, the identity w.r.t. composition of substitutions) and (iii) jV denotes the restriction of the substitution to the set of variables V , that is, the set of ....

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. The MIT Press, 1993.

....semantics is still too complex even if restricted to the relevant language fragment; this is mostly due to the fact that SML contains imperative constructs which are out of the scope of this paper. Instead, we use the more vanilla operational semantics of an eager language following closely [22]. We consider the task of bridging the gap between Real SML in the sense of [14] and our language which we call AbstractSML as routine. 3.1 Expressions of AbstractSML The key ingredient of this operational semantics is an inductively de ned subset of all terms, the so called set of ....

....5.2 The instance FIX The language WF, constrained to total functions, had to rule out values like hd [ or 3 div 0. When admitting partial functions, there is the well known choice for the semantics of function application re ecting call by value evaluation or call by name evaluation (cf. [22]) An appropriate semantical framework for tackling these issues is denotational semantics, which we use as basis for our second program notion FIX. There are many known formalisations of denotational semantics in HOL systems. For Isabelle HOL, there is most notably HOLCF [17] Instead, we will ....

[Article contains additional citation context not shown here]

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993.

.... the problem of specifying all possible action combinations that comprise attacks is essentially the same as specifying all possible behaviors of computational devices (potentially with parallelism and randomization) which is a problem that has received much attention in its own right (e.g. [8]) This solution also ignores the challenges raised by complex correctness properties e.g. if a service must satisfy X or Y , then an allowable sequence of two actions that subvert X and Y respectively may be a vulnerability (unless the second action re enables X) Fully exploring these ....

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993. 1 The ith level has k natural threats, k(i \Gamma 1) inherited threats, and

....rules for T set (A 1 ; A n ) from the typing rules of the constructors by replacing the name T by T set and 0 a i by A i for i 2 [1; n] By the principle of inductive definition, a finite number of rules such as the ones above uniquely specifies a set, c.f. chapter 4 of [8] and the literature cited there. This set is the intersection of all the sets which comply to those rules. Support for inductive definitions in higher order logic proof systems has been described in [3] and [6] Both approaches implement inductively defined sets as least fixed points. Our ....

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing. The MIT Press, 1993.

No context found.

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993. 75

No context found.

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. The MIT Press, 1993.

No context found.

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993. 33

No context found.

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993.

No context found.

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing. The MIT Press, 1993.

No context found.

G. Winskel. The Formal Semantics of Programming Languages: an Introduction. MIT Press, 1993.

No context found.

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge, MA, 1993.

No context found.

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge, MA, 1993.

No context found.

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993.

No context found.

G. Winskel. The Formal Semantics of Programming Languages: an Introduction.

No context found.

Winskel G.: The formal semantics of programming languages: an introduction. MIT Press Series in the Foundations of Computing. London: MIT Press, 1993

No context found.

G. Winskel. The Formal Semantics of Programming Languages: an Introduction. MIT Press, 1993. 22

No context found.

Winskel, G., The Formal Semantics of Programming Languages: An Introduction, MIT Press, 1993.

No context found.

Winskel, G., The Formal Semantics of Programming Languages: An Introduction, MIT Press, 1993.

No context found.

Winskel, G., The Formal Semantics of Programming Languages: An Introduction, MIT Press, 1993.

No context found.

Winskel, G., The Formal Semantics of Programming Languages: An Introduction, MIT Press, 1993.

No context found.

Winskel, G., 1993, The Formal Semantics of Programming Languages: An Introduction. The MIT Press.

No context found.

Winskel, G. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing series. MIT Press, Feb. 1993. 10

First 50 documents  Next 50

Online articles have much greater impact   More about CiteSeer.IST at NUS   Add search form to your site   Submit documents   Feedback  

CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.