LEADER 03349oam  2200553   450 
001 996465490603316
005 20210717111130.0
010   $a3-540-48959-2
024 7 $a10.1007/3-540-48959-2
035   $a(CKB)1000000000211075
035   $a(SSID)ssj0000327457
035   $a(PQKBManifestationID)11294587
035   $a(PQKBTitleCode)TC0000327457
035   $a(PQKBWorkID)10301733
035   $a(PQKB)11568734
035   $a(DE-He213)978-3-540-48959-7
035   $a(MiAaPQ)EBC3073271
035   $a(MiAaPQ)EBC6485750
035   $a(PPN)15522090X
035   $a(EXLCZ)991000000000211075
100   $a20210717d1999      uy             0
101 0 $aeng
135   $aurnn|008mamaa
181   $ctxt
182   $cc
183   $acr
200 00$aTyped lambda calculi and applications $e4th international conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999 : proceedings /$fJean-Yves Girard (editor)
205   $a1st ed. 1999.
210  1$aBerlin :$cSpringer,$d[1999]
210  4$d©1999
215   $a1 online resource (VIII, 404 p.) 
225 1 $aLecture notes in computer science ;$v1581
300   $aBibliographic Level Mode of Issuance: Monograph
311   $a3-540-65763-0 
320   $aIncludes bibliographical references and index.
327   $aInvited 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.
410  0$aLecture notes in computer science ;$v1581.
606   $aLambda calculus$vCongresses
615  0$aLambda calculus
676   $a511.3
702   $aGirard$b Jean-Yves
712 12$aInternational Conference on Typed Lambda Calculi and Applications
801  0$bMiAaPQ
801  1$bMiAaPQ
801  2$bUtOrBLW
906   $aBOOK
912   $a996465490603316
996   $aTyped Lambda Calculi and Applications$9772124
997   $aUNISA