|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNINA9910143465603321 |
|
|
Titolo |
Typed lambda calculi and applications : 4th international conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999 : proceedings / / Jean-Yves Girard (editor) |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin : , : Springer, , [1999] |
|
©1999 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 1999.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (VIII, 404 p.) |
|
|
|
|
|
|
Collana |
|
Lecture notes in computer science ; ; 1581 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Bibliographic Level Mode of Issuance: Monograph |
|
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references and index. |
|
|
|
|
|
|
Nota di contenuto |
|
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: |
|
|
|
|