Мобильная версия

Доступно журналов:

2 361

Доступно статей:

3 493 662

 

Cambridge University Press по журналам "Mathematical Structures in Computer Science"

Отсортировать по: Порядок: Результаты:

  • PAUL THIERRY (Cambridge University Press. Cambridge, UK, 2007-04-01)
    This special issue of Mathematical Structures in Computer Science contains several contributions to the Workshop 3 corps, classique-quantique, discret-continu. The Workshop was held at the Ecole Normale Supérieure, Paris ...
  • FAGORZI SONIA; ZUCCA ELENA (Cambridge University Press. Cambridge, UK, 2007-08-01)
    We present a simple module calculus where selection and execution of a component is possible on open modules, that is, modules that still need to import some external definitions. Hence, it provides a kernel model for a ...
  • Baclawski Kenneth; Simovici Dan; White William (Cambridge University Press. Cambridge, UK, 1994-06-01)
    We propose a formalization of standard database management systems using topos theory. In this treatment, all constructions take place within an ambient topos, which thereby serves as the ‘universe of discourse’. A database ...
  • Ambler Simon (Cambridge University Press. Cambridge, UK, 1996-04-01)
    Argumentation is a proof theoretic paradigm for reasoning under uncertainty. Whereas a ‘proof’ establishes its conclusion outright, an ‘argument’ can only lend a measure of support. Thus, the process of argumentation ...
  • Rosenthal Kimmo I. (Cambridge University Press. Cambridge, UK, 1994-09-01)
    In this article, we indicate how the category theoretical approach to tree automata, due to Betti and Kasangian, can be fruitfully combined with Walters’ categorical approach to context-free grammars to provide a simple ...
  • Goguen Joseph A. (Cambridge University Press. Cambridge, UK, 1991-03-01)
    This paper tries to explain why and how category theory is useful in computing science, by giving guidelines for applying seven basic categorical concepts: category, functor, natural transformation, limit, adjoint, colimit ...
  • Moggi Eugenio (Cambridge University Press. Cambridge, UK, 1991-03-01)
    The type-theoretic explanation of modules proposed to date (for programming languages like ML) is unsatisfactory, because it does not capture that the evaluation of type-expressions is independent from the evaluation of ...
  • Rozière Paul (Cambridge University Press. Cambridge, UK, 1993-06-01)
    This paper gives some sufficient conditions for admissible rules to be derivable in intuitionistic propositional calculus. For example, if the premises are Harrop formulas, the rule is admissible only if it is derivable. ...
  • Power A. J.; Wells Charles (Cambridge University Press. Cambridge, UK, 1992-03-01)
    A type of higher-order two-dimensional sketch is defined which has models in suitable 2-categories. It has as special cases the ordinary sketches of Ehresmann and certain previously defined generalizations of one-dimensional ...
  • HARRISON JOHN (Cambridge University Press. Cambridge, UK, 2011-07-01)
    Pick's Theorem relates the area of a simple polygon with vertices at integer lattice points to the number of lattice points in its inside and boundary. We describe a formal proof of this theorem using the HOL Light theorem ...
  • HARRISON JOHN (Cambridge University Press. Cambridge, UK, 2011-07-01)
    Pick's Theorem relates the area of a simple polygon with vertices at integer lattice points to the number of lattice points in its inside and boundary. We describe a formal proof of this theorem using the HOL Light theorem ...
  • BERTOT YVES; GUILHOT FRÉDÉRIQUE; MAHBOUBI ASSIA (Cambridge University Press. Cambridge, UK, 2011-07-01)
    Bernstein coefficients provide a discrete approximation of the behaviour of a polynomial inside an interval. This can be used, for example, to isolate the real roots of polynomials. We prove formally a criterion for the ...
  • BERTOT YVES; GUILHOT FRÉDÉRIQUE; MAHBOUBI ASSIA (Cambridge University Press. Cambridge, UK, 2011-07-01)
    Bernstein coefficients provide a discrete approximation of the behaviour of a polynomial inside an interval. This can be used, for example, to isolate the real roots of polynomials. We prove formally a criterion for the ...
  • Connelly Richard H.; Morris F. Lockwood (Cambridge University Press. Cambridge, UK, 1995-09-01)
    Tries, a form of string-indexed look-up structure, are generalized, in a manner first discovered by Wadsworth, to permit indexing by terms built according to an arbitrary signature. The construction is parametric with ...
  • BAETEN JOS C. M.; BRAVETTI MARIO (Cambridge University Press. Cambridge, UK, 2008-12-01)
    The three classical process algebras CCS, CSP and ACP present several differences in their respective technical machinery. This is due, not only to the difference in their operators, but also to the terminology and ‘way ...
  • BAETEN JOS C. M.; BRAVETTI MARIO (Cambridge University Press. Cambridge, UK, 2008-12-01)
    The three classical process algebras CCS, CSP and ACP present several differences in their respective technical machinery. This is due, not only to the difference in their operators, but also to the terminology and ‘way ...
  • Padberg Julia; Ehrig Hartmut; Ribeiro Leila (Cambridge University Press. Cambridge, UK, 1995-06-01)
    The concept of algebraic high-level net transformation systems combines two important lines of research recently introduced in the literature: algebraic high-level nets (AHL-nets for short) and high-level replacement systems ...
  • Orejas Fernando; Navarro Marisa; Sánchez Ana (Cambridge University Press. Cambridge, UK, 1996-02-01)
    In this paper we try to shed some light on the similarities and differences in the different approaches denning the notions of implementation and implementation correctness. For obvious reasons, we do not discuss all ...
  • Obtułowicz Adam (Cambridge University Press. Cambridge, UK, 1993-03-01)
    We present an algebraic approach to the syntax and semantics of Martin-Löf type theory and the calculus of constructions developed by T. Coquand and G. Huet. In our approach, models of this theory and this calculus are ...
  • O'Hearn P. W. (Cambridge University Press. Cambridge, UK, 1993-12-01)
    Two imperative programming language phrases interfere when one writes to a storage variable that the other reads from or writes to. Reynolds has described an elegant linguistic approach to controlling interference in which ...