Proceedings - Symposium on Logic in Computer Science
SCOPUS (1986-1987,1990-2011,2013,2015-2019,2021-2023)
1043-6871
Mỹ
Cơ quản chủ quản: Institute of Electrical and Electronics Engineers Inc.
Lĩnh vực:
SoftwareMathematics (miscellaneous)
Các bài báo tiêu biểu
The powerdomain of indexed valuations
- 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
Dense real-time games
- Trang 167-176
The rapid development of complex and safety-critical systems requires the use of reliable verification methods and tools for system design (synthesis). Many systems of interest are reactive, in the sense that their behavior depends on the interaction with the environment. A natural framework to model them is a two-player game: the system versus the environment. In this context, the central problem......
#Automata #Clocks #Logic #Timing #Computer science #Open systems #Real time systems #Tree graphs #Indium tin oxide #Game theory
A fully abstract may testing semantics for concurrent objects
- Trang 101-112
This paper provides a fully abstract semantics for a variant of the concurrent object calculus. We define may testing for concurrent object components and then characterise it using a trace semantics inspired by UML interaction diagrams. The main result of this paper is to show that the trace semantics is fully abstract for may testing. This is the first such result for a concurrent object languag......
#Testing #Calculus #Unified modeling language #Yarn #Production facilities #Safety #Robustness #Visualization #Jacobian matrices #Standards development
Probabilistic abstraction for model checking: an approach based on property testing
- Trang 30-39
The goal of model checking is to verify the correctness of a given program, on all its inputs. The main obstacle, in many cases, is the intractably large size of the program's transition system. Property testing is a randomized method to verify whether some fixed property holds on individual inputs, by looking at a small random part of that input. We join the strengths of both approaches by introd......
#Logic #Computer science #Concrete #System testing #Complexity theory #Combinatorial mathematics #Application software #Sampling methods #Computer languages #Data structures
Computational adequacy for recursive types in models of intuitionistic set theory
- Trang 287-298
We present a general axiomatic construction of models of FPC, a recursively typed lambda-calculus with call-by-value operational semantics. Our method of construction is to obtain such models as full subcategories of categorical models of intuitionistic set theory. This allows us to obtain a notion of model that encompasses both domain-theoretic and realizability models. We show that the existence......
#Set theory #Flexible printed circuits #Equations #Sufficient conditions #Informatics #Computational modeling #Logic #Computer science
Remarks on isomorphisms in typed lambda calculi with empty and sum types
- Trang 147-156
Tarski asked whether the arithmetic identities taught in high school are complete for showing all arithmetic equations valid for the natural numbers. The answer to this question for the language of arithmetic expressions using a constant for the number one and the operations of product and exponentiation is affirmative, and the complete equational theory also characterises isomorphism in the typed......
#Equations #Digital arithmetic #Educational institutions #Computer languages #Calculus #Logic programming #Functional programming #Algebra #Laboratories #Libraries
Semantic subtyping
- 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
Polarized games
- Trang 265-274
We generalize the intuitionistic Hyland-Ong games to a notion of polarized games allowing games with plays starting by proponent moves. The usual constructions on games are adjusted to fit this setting yielding a game model for polarized linear logic with a definability result. As a consequence this gives a complete game model for various classical systems: LC, /spl lambda//spl mu/-calculus,... fo......
#Polarization #Logic programming #Computer languages #Waste materials #Computer science #Embedded computing
Semantic minimization of 3-valued propositional formulae
- Trang 40-51
This paper presents an algorithm for a non-standard logic-minimization problem that arises in 3-valued propositional logic. The problem is motivated by the potential for obtaining better answers in applications that use 3-valued logic. An answer of 0 or 1 provides precise (definite) information; an answer of 1/2 provides imprecise (indefinite) information. By replacing a formula /spl phi/ with a "......
#Logic #Hardware #Data analysis #Information analysis #Software systems #Uncertainty #Contracts #Terminology #Minimization methods
The 0-1 law fails for frame satisfiability of propositional modal logic
- 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