Typed lambda calculi and applications : 4th international conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999 : proceedings
Wedi'i Gadw mewn:
| Awdur Corfforaethol: | |
|---|---|
| Awduron Eraill: | |
| Fformat: | Livre numérique |
| Iaith: | Anglais |
| Cyhoeddwyd: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Cyfres: | Lecture notes in computer science
1581 |
| Pynciau: | |
| Mynediad Ar-lein: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Nodyn: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Typed lambda calculi and applications, 4th international conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, proceedings, Jean-Yves Girard (ed), 1999, New York, Springer, 1 vol. (VIII-396 p.), Lecture notes in computer science, 3-540-65763-0 • Typed Lambda Calculi and Applications, Texte imprimé, 9783662185056 |
Tabl Cynhwysion:
- 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.