Intensional logic is applied to the semantics of an Algol-like programming language. this approach associates with expressions their senses, or meanings relative to possible worlds, here interpreted as machine states....
详细信息
ISBN:
(纸本)081862230X
Intensional logic is applied to the semantics of an Algol-like programming language. this approach associates with expressions their senses, or meanings relative to possible worlds, here interpreted as machine states. these meanings lie in the semantic domains of a higher order typed intensional logic. the advantage of the approach is that it preserves compositionality of the meaning function, even in opaque contexts. this study extends earlier work in this direction, by T. M. V. Janssen and P. Van Emde Boas (1977), to pointers, including dereferenced pointers on both sides of assignments. It is shown how this approach gives an elegant solution to the problem of pointer semantics which is simple, compositional, and implementation independent.
It is shown how to interpret classical proofs as programs in a way that agrees withthe well-known treatment of constructive proofs as programs and moreover extends it to give a computational meaning to proofs claimin...
详细信息
ISBN:
(纸本)081862230X
It is shown how to interpret classical proofs as programs in a way that agrees withthe well-known treatment of constructive proofs as programs and moreover extends it to give a computational meaning to proofs claiming the existence of a value satisfying a recursive predicate. the method turns out to be equivalent to H. Friedman's (Lecture Notes in Mathematics, vol. 699, pp. 21-28, 1978) proof by A-transition of the conservative extension of classical cover constructive arithmetic for II20 sentences. It is shown that Friedman's result is a proof-theoretic version of a semantics-preserving CPS-translation from a nonfunctional programming language back to a functional programming language. A sound evaluation semantics for proofs in classical number theory (PA) of such sentences is presented as a modification of the standard semantics for proofs in constructive number theory (HA). the results soundly extend the proofs-as-programs paradigm to classical logics and to programs withthe control operator, C.
Computational open-endedness in a type theory is defined as the property that theorems remain true under extensions to the underlying programming language. Some properties related to open-endness that are relevant to ...
详细信息
ISBN:
(纸本)081862230X
Computational open-endedness in a type theory is defined as the property that theorems remain true under extensions to the underlying programming language. Some properties related to open-endness that are relevant to machine implementations of type theory are established. A class of computation systems, specified by a simple but fairly general kind of structural operational semantics, with respect to which P. Martin-Lof's (6th Int. Congress for Logic, Methodology, and Philosophy of Science, pp. 153-175, 1982) type theory (and most of its descendants) is open-ended is defined. It is shown that any such system validates a useful form of type free reasoning about program equivalence and that symbolic computation procedures can be automatically derived from these specifications. the main result is the definition of a particular computation system that includes a collection of oracles sufficient to provide a classical semantics for Martin-Lof's type theory in which the law of the excluded middle holds.
the proceedings contain 61 papers. the special focus in this conference is on mathematicalfoundations of Computer Science. the topics include: Frequency algorithms and computations;graph-theoretic arguments in low-le...
ISBN:
(纸本)9783540083535
the proceedings contain 61 papers. the special focus in this conference is on mathematicalfoundations of Computer Science. the topics include: Frequency algorithms and computations;graph-theoretic arguments in low-level complexity;properties of complexity classes a short survey;a uniform approach to inductive posets and inductive closure;generalized probabilistic grammars;classes of structurally isomorphic np-optimization problems;pushdown-automata and families of languages generating cylinders;semantics of infinite processes using generalized trees;a comparative review of some program verification methods;characterization of recognizable families by means of regular languages;an algebraic approach to problem solution and problem semantics;complexity and minimality of context-free grammars and languages;comparison of the active visiting and the crossing complexities;arithmetical complexity of some problems in computer science;formal transformations and the development of programs;optimal rasp programs for arbitrarily complex 0–1 valued functions;the expressive power of intensional logic in the semantics of programming languages;on the complexity of equivalent transformations in programming languages;Schematology in a MJ I/T I-language OPT imizer;classification of the context-free languages;decidability (undecidability) of equivalence of Minsky machines with components consisting of at most seven (eight) instructions;a top-down no backtrack parsing of general context-free languages;a probabilistic restriction of branching plans;reducing operators for normed general formal systems;invariant properties of informational bulks;two decidability results for deterministic pushdown automata;on the logic of incomplete information;measures of ambiguity in the analysis of complex systems;two-level meta-controlled substitution grammars;a calculus to build up correct programs;acceptors for iteration languages.
the relative stabilization in language design and schematology, which succeeded to their rapid growth in 1960s, puts forward the problem of practical synthesis of their achievements. We have reviewed the experience ga...
详细信息
this paper presents a simple algebraic description of the semantics of non-deterministic recursive flow diagram programs with parallel assignment, culminating in a method for proving their partial correctness which ge...
详细信息
this book constitutes the refereed proceedings of the 6th International workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2018, held in Gold Coast, Australia60;in November 2018.;the 10 revised full p...
详细信息
ISBN:
(数字)9783030129880
ISBN:
(纸本)9783030129873
this book constitutes the refereed proceedings of the 6th International workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2018, held in Gold Coast, Australia in November 2018.;the 10 revised full papers presented together with an abstract of an invited talk were carefully reviewed and selected from 22 submissions. the papers are organized in topical sections on analysis and verification of Safety-Critical Systems; analysis of timed systems; semantics and analysis methods, and model transformation.
暂无评论