LEADER 05681nam 22006855 450 001 996466077903316 005 20200707032124.0 010 $a3-540-47586-9 024 7 $a10.1007/BFb0037093 035 $a(CKB)1000000000233943 035 $a(SSID)ssj0000327454 035 $a(PQKBManifestationID)11294586 035 $a(PQKBTitleCode)TC0000327454 035 $a(PQKBWorkID)10301401 035 $a(PQKB)10724948 035 $a(DE-He213)978-3-540-47586-6 035 $a(PPN)155225944 035 $a(EXLCZ)991000000000233943 100 $a20121227d1993 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aTyped Lambda Calculi and Applications$b[electronic resource] $eInternational Conference on Typed Lambda Calculi and Applications, TLCA '93, March 16-18, 1993, Utrecht, The Netherlands. Proceedings /$fedited by Marc Bezem, Jan F. Groote 205 $a1st ed. 1993. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1993. 215 $a1 online resource (IX, 443 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v664 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-56517-5 327 $aOn Mints' reduction for ccc-calculus -- A formalization of the strong normalization proof for System F in LEGO -- Partial intersection type assignment in applicative term rewriting systems -- Extracting constructive content from classical logic via control-like reductions -- Combining first and higher order rewrite systems with type assignment systems -- A term calculus for Intuitionistic Linear Logic -- Program extraction from normalization proofs -- A semantics for ? &-early: a calculus with overloading and early binding -- An abstract notion of application -- The undecidability of typability in the Lambda-Pi-calculus -- Recursive types are not conservative over F? -- The conservation theorem revisited -- Modified realizability toposes and strong normalization proofs -- Semantics of lambda-I and of other substructure lambda calculi -- Translating dependent type theory into higher order logic -- Studying the fully abstract model of PCF within its continuous function model -- A new characterization of lambda definability -- Combining recursive and dynamic types -- Lambda calculus characterizations of poly-time -- Pure type systems formalized -- Orthogonal higher-order rewrite systems are confluent -- Monotonic versus antimonotonic exponentiation -- Inductive definitions in the system Coq rules and properties -- Intersection types and bounded polymorphism -- A logic for parametric polymorphism -- Call-by-value and nondeterminism -- Lower and upper bounds for reductions of types in ? and ?P (extended abstract) -- ?-Calculi with conditional rules -- Type reconstruction in F? is undecidable. 330 $aThe lambda calculus was developed in the 1930s by Alonzo Church. The calculus turned out to be an interesting model of computation and became theprototype for untyped functional programming languages. Operational and denotational semantics for the calculus served as examples for otherprogramming languages. In typed lambda calculi, lambda terms are classified according to their applicative behavior. In the 1960s it was discovered that the types of typed lambda calculi are in fact appearances of logical propositions. Thus there are two possible views of typed lambda calculi: - as models of computation, where terms are viewed as programs in a typed programming language; - as logical theories, where the types are viewed as propositions and the terms as proofs. The practical spin-off from these studies are: - functional programming languages which are mathematically more succinct than imperative programs; - systems for automated proof checking based on lambda caluli. This volume is the proceedings of TLCA '93, the first international conference on Typed Lambda Calculi and Applications,organized by the Department of Philosophy of Utrecht University. It includes29 papers selected from 51 submissions. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v664 606 $aComputers 606 $aMathematical logic 606 $aComputer logic 606 $aComputer programming 606 $aTheory of Computation$3https://scigraph.springernature.com/ontologies/product-market-codes/I16005 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 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aProgramming Techniques$3https://scigraph.springernature.com/ontologies/product-market-codes/I14010 615 0$aComputers. 615 0$aMathematical logic. 615 0$aComputer logic. 615 0$aComputer programming. 615 14$aTheory of Computation. 615 24$aMathematical Logic and Foundations. 615 24$aMathematical Logic and Formal Languages. 615 24$aLogics and Meanings of Programs. 615 24$aProgramming Techniques. 676 $a511.3 702 $aBezem$b Marc$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aGroote$b Jan F$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aInternational Conference on Typed Lambda Calculi and Applications 906 $aBOOK 912 $a996466077903316 996 $aTyped Lambda Calculi and Applications$9772124 997 $aUNISA LEADER 03098nam 2200661Ia 450 001 9910963693103321 005 20150526173120.0 010 $a1-78441-781-5 035 $a(CKB)3710000000410179 035 $a(EBL)2054909 035 $a(SSID)ssj0001540477 035 $a(PQKBManifestationID)11906685 035 $a(PQKBTitleCode)TC0001540477 035 $a(PQKBWorkID)11533922 035 $a(PQKB)10103570 035 $a(MiAaPQ)EBC2054909 035 $a(Au-PeEL)EBL2054909 035 $a(CaPaEBR)ebr11055518 035 $a(CaONFJC)MIL784699 035 $a(OCoLC)913843019 035 $a(UtOrBLW)bslw09340704 035 $a(EXLCZ)993710000000410179 100 $a20150526d2015 uy 0 101 0 $aeng 135 $aurun||||||||| 181 $ctxt 182 $cc 183 $acr 200 00$aResearch in economic history /$fedited by Susan Wolcott and Christopher Hanes 205 $aFirst edition. 210 1$aBingley, England :$cEmerald,$d2015. 210 4$dİ2015 215 $a1 online resource (272 p.) 225 0 $aResearch in economic history,$x0363-3268 ;$v31 300 $a"Emerald Books"--Cover. 311 08$a1-78441-782-3 320 $aIncludes bibliographical references at the end of each chapters. 327 $aDecline and stagnation in the Arab world : preliminary real wage evidence comparing Algeria, Egypt, Syria and Tunisia, 1847-1913 / Paul Caruana-Galizia -- New Deal funding : estimates of federal grants and loans across states by year, 1930-1940 / Price Fishback -- How many calories? food availability in England and Wales in the eighteenth and nineteenth centuries / Bernard Harris, Roderick Floud, Sok Hong -- "Not much use in disliking it" : the work and wages of female home workers in London, 1897-1908 / Jessica Bean -- Capital inflows, current accounts and the investment cycle in Italy : 1861-1913 / Barbara Pistoresi, Alberto Rinaldi. 330 $aVolume 31 of Research in Economic History (REHI) is forthcoming in April 2015. REHI is a peer-reviewed series published once a year. We cover all areas of economic history, including demography and development. Research in Economic History is a well-established and well-cited journal which has presented work by leading researchers in the field of economic history, including economists, historians and demographers. 410 0$aResearch in Economic History 606 $aBusiness & Economics$xEconomic History$2bisacsh 606 $aEconomic theory & philosophy$2bicssc 606 $aEconomic history$xStatistics 606 $aEconomic history 606 $aEconomic indicators 615 7$aBusiness & Economics$xEconomic History. 615 7$aEconomic theory & philosophy. 615 0$aEconomic history$xStatistics. 615 0$aEconomic history. 615 0$aEconomic indicators. 676 $a339.31021 701 $aHanes$b Christopher$0140374 701 $aWolcott$b Susan$01854457 801 0$bUtOrBLW 906 $aBOOK 912 $a9910963693103321 996 $aResearch in economic history$94451768 997 $aUNINA