Typed Lambda Calculi and Applications 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Girard, Jean-Yves (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1999.
• Έκδοση: 1st ed. 1999.
• Σειρά: Lecture Notes in Computer Science, 1581
• Θέματα: Computers.; Mathematical logic.; Computer logic.; Computer programming.; Theory of Computation.; Mathematical Logic and Formal Languages.; Logics and Meanings of Programs.; Programming Techniques.; Mathematical Logic and Foundations.

Πίνακας περιεχομένων:

• Invited Demonstration
• The Coordination Language Facility and Applications
• AnnoDomini in Practice: A Type-Theoretic Approach to the Year 2000 Problem
• Contributions
• Modules in Non-commutative Logic
• Elementary Complexity and Geometry of Interaction
• Quantitative Semantics Revisited
• Total Functionals and Well-Founded Strategies
• Counting a Type's Principal Inhabitants
• Useless-Code Detection and Elimination for PCF with Algebraic Data Types
• Every Unsolvable ? Term has a Decoration
• Game Semantics for Untyped ???-Calculus
• A Finite Axiomatization of Inductive-Recursive Definitions
• Lambda Definability with Sums via Grothendieck Logical Relations
• Explicitly Typed ??-Calculus for Polymorphism and Call-by-Value
• Soundness of the Logical Framework for Its Typed Operational Semantic
• Logical Predicates for Intuitionistic Linear Type Theories
• Polarized Proof-Nets: Proof-Nets for LC
• Call-by-Push-Value: A Subsuming Paradigm
• A Study of Abramsky's Linear Chemical Abstract Machine
• Resource Interpretations, Bunched Implications and the ??-Calculus (Preliminary Version)
• A Curry-Howard Isomorphism for Compilation and Program Execution
• Natural Deduction for Intuitionistic Non-commutative Linear Logic
• A Logic for Abstract Data Types as Existential Types
• Characterising Explicit Substitutions which Preserve Termination
• Explicit Environments
• Consequences of Jacopini's Theorem: Consistent Equalities and Equations
• Strong Normalisation of Cut-Elimination in Classical Logic
• Pure Type Systems with Subtyping.