Typed Lambda Calculi and Applications(有类型Lambda演算及其应用/会议录)

作者简介

The LNCS series reports state-of-the-art results in computer science research，development，and education，at a high level and in both printed and electronic form.Enjoying tight cooperation with the R&D community，with numerous individuals，as well as with prestigious organizations and societies，LNCS has grown into the most comprehensive computer science research forum available.    The scope of LNCS，including its subseries LNAI，spans the whole range of computer science and information technology including interdisciplinary topics in a variety of application fields.The type of material published traditionally includes.    —proceedings （published in time for the respective conference）    —post-proceedings （consisting of thoroughly revised final full papers）    —research monographs（which may be based on outstanding PhD work，research projects，technical reports，etc.）.

书籍目录

Completeness Theorems and A-CalculusA Tutorial Example of the Semantic Approach to FoundationalProof-Carrying Code: AbstractCan Proofs Be Animated by Games?Contributed Papers　Untyped Algorithmic Equality for Martin-LSf's Logical Framework with Surjective PairsThe Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is DecidableA Feasible Algorithm for Typing in Elementary Affine LogicPractical Inference for Type-Based Termination in a Polymorphic SettingRelational Reasoning in a Nominal Semantics for StorageFilters on CoInductive Streams, an Application to Eratosthenes' SieveRecursive Functions with Higher Order DomainsElementary Affine Logic and the Call-by-Value Lambda CalculusRank-2 Intersection and Polymorphic Recursion Aft-CalculusSubtyping Recursive Types Modulo Associative Commutative ProductsGalois Embedding from Polymorphic Types into Existential TypesOn the Degeneracy of Z-Types in Presence of Computational ClassicalLogicSemantic Cut Elimination in the Intuitionistic Sequent CalculusThe Elimination of Nesting in SPCFNaming Proofs in Classical Propositional LogicReducibility and TT-Lifting for Computation TypesPrivacy in Data Mining Using Formal MethodsL3: A Linear Language with LocationsBinding Signatures for Generic ContextsProof Contexts with Late BindingThe V-Calculus. Functional Programming with Higher-Order EncodingsA Lambda Calculus for Quantum Computation with Classical ControlContinuity and Discontinuity in Lambda CalculusAuthor Index

 Typed Lambda Calculi and Applications(有类型Lambda演算及其应用/会议录)下载