this book constitutes the refereed proceedings of the 9thinternationalconference on Typed Lambda Calculi and Applications, TLCA 2009, held in Brasilia, Brazil in July 2008 in conjunction with RTA 2007, the 19th Inte...
详细信息
ISBN:
(数字)9783642022739
ISBN:
(纸本)9783642022722
this book constitutes the refereed proceedings of the 9thinternationalconference on Typed Lambda Calculi and Applications, TLCA 2009, held in Brasilia, Brazil in July 2008 in conjunction with RTA 2007, the 19thinternationalconference on Rewriting Techniques and Applications as part of RDP 2009, the 5thinternationalconference on Rewriting, Deduction, and programming. the 27 revised full papers presented together with 2 invited talks were carefully reviewed and selected from 53 submissions. the papers present original research results that are broadly relevant to the theory and applications of typed calculi and address a wide variety of topics such as proof-theory, semantics, implementation, types, and programming.
the proceedings contain 29 papers. the topics discussed include: exploiting algebraic laws to improve mechanized axiomatizations;positive fragments of coalgebraiclogics;many-valued relation lifting and moss' coal...
ISBN:
(纸本)9783642402050
the proceedings contain 29 papers. the topics discussed include: exploiting algebraic laws to improve mechanized axiomatizations;positive fragments of coalgebraiclogics;many-valued relation lifting and moss' coalgebraiclogic;saturated semantics for coalgebraiclogicprogramming;presenting distributive laws;interaction and observation: categorical semantics of reactive systems trough dialgebras;homomorphisms of coalgebras from predicate liftings;trace semantics via generic observations;full abstraction for fair testing in CCS;a simple case of rationality of escalation;coalgebras with symmetries and modeling quantum systems;from operational chu duality to coalgebraic quantum symmetry;noninterfering schedulers: when possibilistic noninterference implies probabilistic noninterference;and simulations and bisimulations for coalgebraic modal logics.
the proceedings contain 25 papers. the special focus in this conference is on programming. the topics include: Procedures and concurrency: A study in proof;another characterization of weakest preconditions;powerdomain...
ISBN:
(纸本)9783540114949
the proceedings contain 25 papers. the special focus in this conference is on programming. the topics include: Procedures and concurrency: A study in proof;another characterization of weakest preconditions;powerdomains and nondeterministic recursive definitions;optimizing for a multiprocessor: Balancing synchronization costs against parallelism in straight-line code;the simple semantics for Coppo-Dezani-Sallé types;proving the correctness of implementations of shared data abstractions;specification of communicating processes and process implementation correctness;a system for reasoning within and about algebraic specifications;tuning algebraic specifications by type merging;a machine-level semantics for nondeterministic, parallel programs;communicating agents for applicative concurrent programming;on effective computations of non-deterministic schemes;Specification and verification of concurrent systems in CESAR;proof of separability A verification technique for a class of security kernels;a method for program synthesis;the use of transformations to implement an algorithm;a formalized proof system for total correctness of while programs;automatic program transformation viewed as theorem proving;an enlarged definition and complete axiomatization of observational congruence of finite processes;perluette : A compilers producing system using abstract data types;a weakest precondition semantics for communicating processes;from abstract model to efficient compilation of patterns;computer-based synthesis of logic programs.
A term rewriting system is strongly innermost normalizing if every innermost derivation of it is of finite length. this property is very important in the integration of functional and logicprogramming paradigms. Unli...
详细信息
this paper presents the design and modeling issues of the fuzzy/scalar processor which is intended to perform standard scalar operations, as well as specialized fuzzy logic operations at very high speed. the reduced i...
详细信息
ISBN:
(纸本)0780336461
this paper presents the design and modeling issues of the fuzzy/scalar processor which is intended to perform standard scalar operations, as well as specialized fuzzy logic operations at very high speed. the reduced instruction set (RISC) architecture was chosen for the processor implementation. this high performance and, at the same time, extremely flexible device, can be used in a variety of applications where high speed standard and/or fuzzy logic operations are required. the high-level simulation results of the fuzzy/scalar reduced instruction set processor model (codename F/S RISC), are presented. the model built with Mentor Graphics' ″M″ language was simulated using Lsim simulator at the clock frequency of 100 MHz. the current technology for the implementation of F/S RISC processor is chosen to be 1.2 μm n-well CMOS.
We propose a sound and complete free variable semantic tableau method for handling many-sorted preorders in a first order logic, where functions and predicates behave monotonically or antimonotonically. We formulate a...
详细信息
Multiset rewriting has proved to be a useful presentation of process synchronization [1, 2, 3, 6]. Since sequent calculus presentations of logics that do not use the structural rules of contractions and weakening are ...
详细信息
ISBN:
(纸本)9783540584315
Multiset rewriting has proved to be a useful presentation of process synchronization [1, 2, 3, 6]. Since sequent calculus presentations of logics that do not use the structural rules of contractions and weakening are based on using multisets of formulas as left and right contexts, it is natural to identify processes with formulas, multisets with sequent contexts, and multiset rewriting as an inference rule. Given earlier work on using sequent calculus to describe logicprogramming as goal-directed search for proofs [8], it is most natural to use right-hand contexts of sequents to represent multisets of processes. this choice requires the identification of the multiset constructor and the empty multiset withthe multiplicative disjunction and false (the and ⊥ of linear logic [4]), and backchaining with a single step of multiset rewriting. While the logicprogramming language λ Prolog [10] and its linear logic refinement Lolli [5] contain rich sources of abstraction (such as modular programming, abstract data types, and higher-order programming), they contain no primitives for specifying concurrency, communications, or synchronization. If multiset rewriting is added to Lolli via the logical connectives and ⊥, the result is a language that contains primitives for both abstraction and concurrency. Surprisingly, the resulting logic, called Forum [7], is a presentation of all of linear logic in the sense that all of the connectives of linear logic can be defined via logical equivalences using only the connectives of Forum. thus the rich meta-theory of linear logic, for example, the de Morgan dualities and cut-elimination, can be applied to the analysis of Forum programs. Several examples to illustrate the expressiveness of this presentation of linear logic will be given. these examples will involve a specification of sequent calculi for object-level logics, a specification of the π-calculus [9], and a specification of a functional programming language that contains side-e
暂无评论