Proceedings - Symposium on Logic in Computer Science
Công bố khoa học tiêu biểu
* Dữ liệu chỉ mang tính chất tham khảo
Sắp xếp:
Domain theory and differential calculus (functions of one variable)
Proceedings - Symposium on Logic in Computer Science - - Trang 277-286
A data-type for differential calculus is introduced, which is based on domain
theory. We define the integral and also the derivative of a Scott continuous
function on the domain of intervals, and present a domain-theoretic
generalization of the fundamental theorem of calculus. We then construct a
domain for differentiable real valued functions of a real variable. The set of
classical C/sup 1/ func...
#Calculus #Differential equations #Polynomials #Educational institutions #Pathology #Mathematics #Approximation algorithms #Uncertainty #Application software #Logic design
Calibrating computational feasibility by abstraction rank
Proceedings - Symposium on Logic in Computer Science - - Trang 345-354
We characterize computationally the functions provable in second order logic
with set existence restricted to natural classes of first order formulas. A
classification of first-order set-existence by implicational rank yields a
natural hierarchy of complexity classes within the class of Kalmar-elementary
functions: The functions over {0, 1}* constructively provable using set
existence for formulas...
#Equations #Arithmetic #Logic #Computational complexity #Mathematics #Mathematical programming #Reasoning about programs #Calculus #Calibration #Size control
Modal and guarded characterisation theorems over finite transition systems
Proceedings - Symposium on Logic in Computer Science - - Trang 371-380
Characterisation theorems for modal and guarded fragments of first-order logic
are explored over finite transition systems. We show that the classical
characterisations in terms of semantic invariance under the appropriate forms of
bisimulation equivalence can be recovered at the level of finite model theory.
The new, more constructive proofs naturally extend to alternative proofs of the
classical...
#Logic #H infinity control #Game theory #Computer science
The powerdomain of indexed valuations
Proceedings - Symposium on Logic in Computer Science - - Trang 299-308
This paper is about combining nondeterminism and probabilities. We study this
phenomenon from a domain theoretic point of view. In domain theory,
nondeterminism is modeled using the notion of powerdomain, while probability is
modeled using the powerdomain of valuations. Those two functors do not combine
well, as they are. We define the notion of powerdomain of indexed valuations,
which can be comb...
#Cost accounting #Equations #Computer science #Laboratories #Computational modeling #Probability distribution #Algebra #Logic #Character generation
The 0-1 law fails for frame satisfiability of propositional modal logic
Proceedings - Symposium on Logic in Computer Science - - Trang 225-234
The digraph property KERNEL is a very simple and wellknown property studied in
various areas. We previously defined a variant of this property as a
counterexample of 0-1 law for the monadic existential second order logic with at
most two first-order variables, over structures with 16 binary relations.
Goranko and Kapron have defined two variants in frames which expresses frame
satisfiability of pr...
#Logic #Kernel #Vocabulary #Bars #Computational modeling #Computational complexity #Combinatorial mathematics #H infinity control
Semantics and logic of object calculi
Proceedings - Symposium on Logic in Computer Science - - Trang 113-122
The main contribution of this paper is a formal characterization of recursive
object specifications based on a denotational untyped semantics of the object
calculus and the discussion of existence of those (recursive) specifications.
The semantics is then applied to prove soundness of a programming logic for the
object calculus and to suggest possible extensions. For the purposes of this
discussio...
#Logic programming #Calculus #Object oriented programming #Machinery #Object oriented modeling #Computer science
Proceedings 17th Annual IEEE Symposium on Logic in Computer Science
Proceedings - Symposium on Logic in Computer Science - - 2002
Presents the front cover of the proceedings record.
Games on graphs and sequentially realizable functionals. Extended abstract
Proceedings - Symposium on Logic in Computer Science - - Trang 257-264
We present a new category of games on graphs and derive from it a model for
Intuitionistic Linear Logic. Our category has the computational flavour of
concrete data structures but embeds fully and faithfully in an abstract games
model. It differs markedly from the usual Intuitionistic Linear Logic setting
for sequential algorithms. However, we show that with a natural exponential we
obtain a model...
#Logic #Concrete #Computer science #Data structures #Mathematical model #Embedded computing #Algorithm design and analysis #Tree graphs
Semantic subtyping
Proceedings - Symposium on Logic in Computer Science - - Trang 137-146
Usually subtyping relations are defined either syntactically by a formal system
or semantically by an interpretation of types in an untyped denotational model.
In this paper we show how to define a subtyping relation semantically, for a
language whose operational semantics is driven by types; we consider a rich type
algebra, with product, arrow, recursive, intersection, union and complement
types....
#Algebra #XML #Programming profession #Databases
On the lambda Y calculus
Proceedings - Symposium on Logic in Computer Science - - Trang 159-166
In this paper we consider three problems concerning the lambda Y calculus
obtained from the simply typed lambda calculus by the addition of fixed point
combinators Y: (A/spl rarr/A)/spl rarr/A. The "paradoxical" combinator Y was
first discussed in by Curry & Feys Vol 1 (1958). It appears first in a typed
context by A. Scott (1969) and also by R. Platek's thesis (1963), and forms the
basis for L. C...
#Calculus #Magnetic heads #Encoding #Equations #Logic #Computer science #Standardization
Tổng số: 42
- 1
- 2
- 3
- 4
- 5