Cambridge University Press по журналам "Mathematical Structures in Computer Science"
Отображаемые элементы 120 из 330

(Cambridge University Press. Cambridge, UK, 20070401)This special issue of Mathematical Structures in Computer Science contains several contributions to the Workshop 3 corps, classiquequantique, discretcontinu. The Workshop was held at the Ecole Normale Supérieure, Paris ...

(Cambridge University Press. Cambridge, UK, 20070801)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 ...

(Cambridge University Press. Cambridge, UK, 19940601)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 ...

(Cambridge University Press. Cambridge, UK, 19960401)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 ...

(Cambridge University Press. Cambridge, UK, 19940901)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 contextfree grammars to provide a simple ...

(Cambridge University Press. Cambridge, UK, 19910301)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 ...

(Cambridge University Press. Cambridge, UK, 19910301)The typetheoretic explanation of modules proposed to date (for programming languages like ML) is unsatisfactory, because it does not capture that the evaluation of typeexpressions is independent from the evaluation of ...

(Cambridge University Press. Cambridge, UK, 19930601)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. ...

(Cambridge University Press. Cambridge, UK, 19920301)A type of higherorder twodimensional sketch is defined which has models in suitable 2categories. It has as special cases the ordinary sketches of Ehresmann and certain previously defined generalizations of onedimensional ...

(Cambridge University Press. Cambridge, UK, 20110701)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 ...

(Cambridge University Press. Cambridge, UK, 20110701)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 ...

(Cambridge University Press. Cambridge, UK, 20110701)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 ...

(Cambridge University Press. Cambridge, UK, 20110701)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 ...

(Cambridge University Press. Cambridge, UK, 19950901)Tries, a form of stringindexed lookup 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 ...

(Cambridge University Press. Cambridge, UK, 20081201)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 ...

(Cambridge University Press. Cambridge, UK, 20081201)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 ...

(Cambridge University Press. Cambridge, UK, 19950601)The concept of algebraic highlevel net transformation systems combines two important lines of research recently introduced in the literature: algebraic highlevel nets (AHLnets for short) and highlevel replacement systems ...

(Cambridge University Press. Cambridge, UK, 19960201)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 ...

(Cambridge University Press. Cambridge, UK, 19930301)We present an algebraic approach to the syntax and semantics of MartinLö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 ...

(Cambridge University Press. Cambridge, UK, 19931201)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 ...
Отображаемые элементы 120 из 330