LEADER 01185nam--2200373---4500 001 990000906640203316 005 20100708093131.0 010 $a88-269-0021-3 035 $a0090664 035 $aUSA010090664 035 $a(ALEPH)000090664USA01 035 $a0090664 100 $a20020128d1991----km-y0ENGy0103----ba 101 $aita 102 $aIT 200 1 $aVersamento dei contributi INPS$eguida pratica alla compilazione delle denunce DM 10/89$gGiuseppe Passeggio, Massimo Rossi 210 $aMilano$cProfessione impresa$d1991 215 $aXI, 266 p.$d21 cm 410 $12001 606 $aContributi di previdenza$xProntuari 676 $a658.321 700 1$aPASSEGGIO,$bGiuseppe$0551844 701 1$aROSSI,$bMassimo$082308 801 0$aIT$bsalbc$gISBD 912 $a990000906640203316 951 $aXXIV.5.C. 414 (COLL. PFN 3)$b2963 EC$cXXIV.5.C. 414 (COLL. PFN)$d00285155 959 $aBK 969 $aECO 979 $aPATTY$b90$c20020128$lUSA01$h1009 979 $c20020403$lUSA01$h1734 979 $aPATRY$b90$c20040406$lUSA01$h1702 979 $aRSIAV2$b90$c20100708$lUSA01$h0931 996 $aVersamento dei contributi INPS$9970558 997 $aUNISA 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