LEADER 04168nam  22007215  450 
001 9910768472203321
005 20200630025157.0
010   $a3-540-44904-3
024 7 $a10.1007/3-540-44904-3
035   $a(CKB)1000000000212052
035   $a(SSID)ssj0000327453
035   $a(PQKBManifestationID)11266284
035   $a(PQKBTitleCode)TC0000327453
035   $a(PQKBWorkID)10316473
035   $a(PQKB)10944842
035   $a(DE-He213)978-3-540-44904-1
035   $a(MiAaPQ)EBC3071901
035   $a(PPN)155204750
035   $a(EXLCZ)991000000000212052
100   $a20121227d2003      u|         0
101 0 $aeng
135   $aurnn|008mamaa
181   $ctxt
182   $cc
183   $acr
200 10$aTyped Lambda Calculi and Applications $e6th International Conference, TLCA 2003, Valencia, Spain, June 10-12, 2003, Proceedings /$fedited by Martin Hofmann
205   $a1st ed. 2003.
210  1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2003.
215   $a1 online resource (VIII, 320 p.) 
225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v2701
300   $aBibliographic Level Mode of Issuance: Monograph
311   $a3-540-40332-9 
320   $aIncludes bibliographical references and index.
327   $aTermination and Productivity Checking with Continuous Types -- Derivatives of Containers -- Max-Plus Quasi-interpretations -- Inductive Types in the Calculus of Algebraic Constructions -- On Strong Normalization in the Intersection Type Discipline -- Relative Definability and Models of Unary PCF -- Principal Typing in Elementary Affine Logic -- A Logical Framework with Dependently Typed Records -- A Sound and Complete CPS-Translation for ??-Calculus -- Abstraction Barrier-Observing Relational Parametricity -- Encoding of the Halting Problem into the Monster Type and Applications -- Well-Going Programs Can Be Typed -- Parameterizations and Fixed-Point Operators on Control Categories -- Functional In-Place Update with Layered Datatype Sharing -- A Fully Abstract Bidomain Model of Unary FPC -- On a Semantic Definition of Data Independence -- Nondeterministic Light Logics and NP-Time -- Polarized Proof Nets with Cycles and Fixpoints Semantics -- Observational Equivalence and Program Extraction in the Coq Proof Assistant -- Permutative Conversions in Intuitionistic Multiary Sequent Calculi with Cuts -- A Universal Embedding for the Higher Order Structure of Computational Effects.
410  0$aLecture Notes in Computer Science,$x0302-9743 ;$v2701
606   $aMathematical logic
606   $aComputer programming
606   $aProgramming languages (Electronic computers)
606   $aComputer logic
606   $aMathematical Logic and Foundations$3https://scigraph.springernature.com/ontologies/product-market-codes/M24005
606   $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048
606   $aProgramming Techniques$3https://scigraph.springernature.com/ontologies/product-market-codes/I14010
606   $aProgramming Languages, Compilers, Interpreters$3https://scigraph.springernature.com/ontologies/product-market-codes/I14037
606   $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X
615  0$aMathematical logic.
615  0$aComputer programming.
615  0$aProgramming languages (Electronic computers).
615  0$aComputer logic.
615 14$aMathematical Logic and Foundations.
615 24$aMathematical Logic and Formal Languages.
615 24$aProgramming Techniques.
615 24$aProgramming Languages, Compilers, Interpreters.
615 24$aLogics and Meanings of Programs.
676   $a511.3
702   $aHofmann$b Martin$4edt$4http://id.loc.gov/vocabulary/relators/edt
712 12$aInternational Conference on Typed Lambda Calculi and Applications
801  0$bMiAaPQ
801  1$bMiAaPQ
801  2$bMiAaPQ
906   $aBOOK
912   $a9910768472203321
996   $aTyped Lambda Calculi and Applications$9772124
997   $aUNINA