GADTs are at the cutting edge of functional programming and becomemore widely used every day. Nevertheless, the semantic foundations underlying GADTs are not well understood. In this paper we solve this problem by sho...
详细信息
We describe a type theory or metalanguage for constructing and reasoning about higher-order programs with global and local state, and its categorical model. this provides an encapsulation primitive for abstracting glo...
详细信息
We describe a type theory or metalanguage for constructing and reasoning about higher-order programs with global and local state, and its categorical model. this provides an encapsulation primitive for abstracting global state and making it local to an object, so that it is passed only between its invocations. Our calculus and its semantics extend the interpretation of lambda-terms in a Cartesian closed category with a monoidal action on a category of evaluation contexts - the sequoid - which is dual to the action of the function type. this gives an interpretation of a new type constructor which allows the representation of both global state - via "state-passing-style" interpretation which uses it to represent output states - and local state, via encapsulation, which corresponds to the unique map into a final coalgebra for the sequoid. this provides the equational theory of our calculus with a coinduction rule for proving equivalence between objects with local state. We show that this theory is sound and complete with respect to the categorical semantics by constructing a term model and we show that it is consistent by giving a concrete example based on a category of games and strategies previously used to interpret general references.
In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories and directed homotopy theory. We specify a new 'homomorphism' type former for Martin-Lof type the...
详细信息
In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories and directed homotopy theory. We specify a new 'homomorphism' type former for Martin-Lof type theory which is roughly analogous to the identity type former originally introduced by Martin-Lof. the homomorphism type former is meant to capture the notions of morphism (from the theory of categories) and directed path (from directed homotopy theory) just as the identity type former is known to capture the notions of isomorphism (from the theory of groupoids) and path (from homotopy theory). Our main result is an interpretation of these homomorphism types into Cat, the category of small categories. there, the interpretation of each homomorphism type homC(a, b) is indeed the set of morphisms between the objects a and b of the category C. We end the paper with an analysis of the interpretation in Cat with which we argue that our homomorphism types are indeed the directed version of Martin-Lof's identity types.
Probabilistic programming is an increasingly popular formalism for modeling randomness and uncertainty. Designing semantic models for probabilistic programs has been extensively studied, but is technically challenging...
详细信息
Probabilistic programming is an increasingly popular formalism for modeling randomness and uncertainty. Designing semantic models for probabilistic programs has been extensively studied, but is technically challenging. Particular complications arise when trying to account for (i) unstructured control-flow, a natural feature in low-level imperative programs;(ii) general recursion, an extensively used programming paradigm;and (iii) nondeterminism, which is often used to represent adversarial actions in probabilistic models, and to support refinement-based development. this paper presents a denotational-semantics framework that supports the three features mentioned above, while allowing nondeterminism to be handled in different ways. To support both probabilistic choice and nondeterministic choice, the semantics is given over control-flow hyper-graphs. the semantics follows an algebraic approach: it can be instantiated in different ways as long as certain algebraic properties hold. In particular, the semantics can be instantiated to support nondeterminism among either program states or state transformers. We develop a new formalization of nondeterminism based on powerdomains over sub-probability kernels. Semantic objects in the powerdomain enjoy a notion we call generalized convexity, which is a generalization of convexity. As an application, the paper sketches an algebraic framework for static analysis of probabilistic programs, which has been proposed in a companion paper.
LPMLN is a probabilistic extension of answer set programs withthe weight scheme adapted from Markov Logic. We study the concept of strong equivalence in LPMLN, which is a useful mathematical tool for simplifying a pa...
详细信息
LPMLN is a probabilistic extension of answer set programs withthe weight scheme adapted from Markov Logic. We study the concept of strong equivalence in LPMLN, which is a useful mathematical tool for simplifying a part of an LPMLN program without looking at the rest of it. We show that the verification of strong equivalence in LPMLN can be reduced to equivalence checking in classical logic via a reduct and choice rules as well as to equivalence checking under the "soft" logic of here-andthere. the result allows us to leverage an answer set solver for LPMLN strong equivalence checking. the study also suggests us a few reformulations of the LPMLN semantics using choice rules, the logic of here-and-there, and classical logic.
Modern quantum programming languages integrate quantum resources and classical control. they must, on the one hand, be linearly typed to reflect the no-cloning property of quantum resources. On the other hand, high-le...
详细信息
the proceedings contain 35 papers. the special focus in this conference is on Logic, semantics, Automata and theory of programming. the topics include: Minimal and monotone minimal perfect hash functions;equational pr...
ISBN:
(纸本)9783662480564
the proceedings contain 35 papers. the special focus in this conference is on Logic, semantics, Automata and theory of programming. the topics include: Minimal and monotone minimal perfect hash functions;equational properties of fixed point operations in cartesian categories;reversible and irreversible computations of deterministic finite-state devices;uniform generation in trace monoids;stochastization of weighted automata;algebraic synchronization criterion and computing reset words;recurrence function on sturmian words;exponential-size model property for PDL with separating parallel composition;a circuit complexity approach to transductions;classes of languages generated by the kleene star of a word;relating paths in transition systems;weighted automata and logics on graphs;quasiperiodicity and non-computability in tilings;strong inapproximability of the shortest reset word;finitary semantics of linear logic and higher-order model-checking and modal inclusion logic.
this book constitutes the refereed proceedings of the 24th International conference on Logic programming, ICLP 2008, held in Udine, Italy, in December 2008. the 35 revised full papers together with 2 invited talks, 2 ...
详细信息
ISBN:
(数字)9783540899822
ISBN:
(纸本)9783540899815
this book constitutes the refereed proceedings of the 24th International conference on Logic programming, ICLP 2008, held in Udine, Italy, in December 2008. the 35 revised full papers together with 2 invited talks, 2 invited tutorials, 11 papers of the co-located first Workshop on Answer Set programming and Other Computing Paradigms (ASPOCP 2008), as well as 26 poster presentations and the abstracts of 11 doctoral consortium articles were carefully reviewed and selected from 177 initial submissions. the papers cover all issues of current research in logic programming - they are organized in topical sections on applications, algorithms, systems, and implementations, semantics and foundations, analysis and transformations, CHRs and extensions, implementations and systems, answer set programming and extensions, as well as constraints and optimizations.
Yuri Gurevich has played a major role in the discovery and development of - plications of mathematical logic to theoretical and practical computer science. His interests have spanned a broad spectrum of subjects, incl...
详细信息
ISBN:
(数字)9783642150258
ISBN:
(纸本)9783642150241
Yuri Gurevich has played a major role in the discovery and development of - plications of mathematical logic to theoretical and practical computer science. His interests have spanned a broad spectrum of subjects, including decision p- cedures, the monadic theory of order, abstract state machines, formal methods, foundations of computer science, security, and much more. In May 2010, Yuri celebrated his 70th birthday. To mark that occasion, on August 22, 2010,a symposium was held in Brno, the Czech Republic, as a sat- lite event of the 35th International Symposium on mathematicalfoundations of Computer Science (MFCS 2010) and of the 19th EACSL Annual conference on Computer Science Logic (CSL 2010). the meeting received generous support from Microsoft Research. In preparation for this 70th birthday event, we asked Yuri’s colleagues (whether or not they were able to attend the symposium) to contribute to a volume in his honor. this book is the result of that e?ort. the collection of articles herein begins with an academic biography, an annotated list of Yuri’s publications and reports, and a personaltribute by Jan Van den Bussche. these are followed by 28 technical contributions. these articles – though they cover a broad range of topics – represent only a fraction of Yuri’s multiple areas of interest. Each contribution was reviewed by one or two readers. In this regard, the editors wish to thank several anonymous individuals for their assistance.
Lattices are discrete mathematical objects with widespread applications to integer programs as well as modern cryptography. A fundamental problem in both domains is the Closest Vector Problem (popularly known as CVP)....
详细信息
暂无评论