Theoretical Aspects of Computer Software: International Conference TACS '91, Sendai, Japan, September 24-27, 1991. Proceedings

by Takayasu Ito (editor)

A semantics for type checking.- Type inference in polymorphic type discipline.- Monotone recursive definition of predicates and its realizability interpretation.- Adding proof objects and inductive definition mechanisms to frege structures.- From term models to domains.- An abstract interpretation for ML equality kinds.- Full abstraction and the Context Lemma (preliminary report).- An efficiency preorder for processes.- On nets, algebras and modularity.- Towards a complete hierarchy of compositional dataflow models.- Type theory as a foundation for computer science.- What is in a On the semantics of statecharts.- Proving termination of general Prolog programs.- On abstraction and the expressive power of programming languages.- Role of logic programming in the FGCS project.- Authentication and delegation with smart-cards.- Data flow analysis as model checking.- On the adequacy of dependence-based representations for programs with heaps.- From programming-by-example to proving-by-example.- From LP to Programming with constraints.- Polynomial recursion analysis in pascal like programs.- Complexity of proving program correctness.- Some normalization properties of martin-löf's type theory, and applications.- Parametricity of extensionally collapsed term models of polymorphism and their categorical properties.- Programs with continuations and linear logic.- ?-Calculus semantics of object-oriented programming languages.- Wrapper semantics of an object-oriented programming language with state.- Sharing actions and attributes in modal action logic.- First order data types and first order logic.- Efficient program Semantics, logic, complexity.- Principal type-schemes of BCI-lambda-terms.- Intersection and union types.- The coherence of languages with intersection types.- Singleton, union and intersection types for program extraction.- Subtyping + Confluence of ??top reduction in F?.- An extension of system F with subtyping.- Will logicians be replaced by machines?.

788 pages, Paperback

First published September 24, 1991