LEADER 02034nam 2200577 450 001 9910480701803321 005 20180731043853.0 010 $a1-4704-0725-6 035 $a(CKB)3360000000464496 035 $a(EBL)3113777 035 $a(SSID)ssj0000889162 035 $a(PQKBManifestationID)11449084 035 $a(PQKBTitleCode)TC0000889162 035 $a(PQKBWorkID)10876267 035 $a(PQKB)11471324 035 $a(MiAaPQ)EBC3113777 035 $a(PPN)195411935 035 $a(EXLCZ)993360000000464496 100 $a20140902h19841984 uy 0 101 0 $aeng 135 $aur|n|---||||| 181 $ctxt 182 $cc 183 $acr 200 10$aQualitative analysis of the anisotropic Kepler problem /$fJosefina Casasayas and Jaume Llibre 210 1$aProvidence, Rhode Island :$cAmerican Mathematical Society,$d1984. 210 4$dİ1984 215 $a1 online resource (126 p.) 225 1 $aMemoirs of the American Mathematical Society,$x0065-9266 ;$vVolume 52, Number 312 300 $a"November 1984, Volume 52, Number 312 (second of 3 numbers)." 311 $a0-8218-2309-4 320 $aIncludes bibliographical references. 327 $a""(IV.7) A subshift as subsystem of h""""(IV.8) Gutzwiller's Theorem""; ""V: THE FLOW ON NEGATIVE ENERGY LEVELS WHEN 19/8""; ""APPENDIX""; ""REFERENCES"" 410 0$aMemoirs of the American Mathematical Society ;$vVolume 52, Number 312. 606 $aDifferential equations 606 $aDifferentiable dynamical systems 606 $aHamiltonian systems 608 $aElectronic books. 615 0$aDifferential equations. 615 0$aDifferentiable dynamical systems. 615 0$aHamiltonian systems. 676 $a515.3/5 700 $aCasasayas$b Josefina$f1957-$0876710 702 $aLlibre$b Jaume 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910480701803321 996 $aQualitative analysis of the anisotropic Kepler problem$91957592 997 $aUNINA LEADER 05040nam 22007575 450 001 996465861103316 005 20200704222152.0 010 $a3-540-70722-0 024 7 $a10.1007/3-540-61780-9 035 $a(CKB)1000000000234541 035 $a(SSID)ssj0000327464 035 $a(PQKBManifestationID)11247115 035 $a(PQKBTitleCode)TC0000327464 035 $a(PQKBWorkID)10299452 035 $a(PQKB)10754986 035 $a(DE-He213)978-3-540-70722-6 035 $a(PPN)155190849 035 $a(EXLCZ)991000000000234541 100 $a20121227d1996 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aTypes for Proofs and Programs$b[electronic resource] $eInternational Workshop, TYPES '95, Torino, Italy, June 5 - 8, 1995 Selected Papers /$fedited by Stefano Berardi, Mario Coppo 205 $a1st ed. 1996. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1996. 215 $a1 online resource (X, 298 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v1158 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-61780-9 327 $aImplicit coercions in type systems -- A two-level approach towards lean proof-checking -- The greatest common divisor: A case study for program extraction from classical proofs -- Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids -- A constructive proof of the Heine-Borel covering theorem for formal reals -- An application of constructive completeness -- Automating inversion of inductive predicates in Coq -- First order marked types -- Internal type theory -- An application of co-inductive types in Coq: Verification of the alternating bit protocol -- Conservativity of equality reflection over intensional type theory -- A natural deduction approach to dynamic logic -- An algorithm for checking incomplete proof objects in type theory with localization and unification -- Decidability of all minimal models -- Circuits as streams in Coq: Verification of a sequential multiplier -- Context-relative syntactic categories and the formalization of mathematical text -- A simple model construction for the Calculus of Constructions -- Optimized encodings of fragments of type theory in first order logic -- Organization and development of a constructive axiomatization. 330 $aThis volume contains a refereed selection of revised full papers chosen from the contributions presented during the Third Annual Workshop held under the auspices of the ESPRIT Basic Research Action 6453 Types for Proofs and Programs. The workshop took place in Torino, Italy, in June 1995. Type theory is a formalism in which theorems and proofs, specifications and programs can be represented in a uniform way. The 19 papers included in the book deal with foundations of type theory, logical frameworks, and implementations and applications; all in all they constitute a state-of-the-art survey for the area of type theory. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v1158 606 $aMathematical logic 606 $aSoftware engineering 606 $aComputers 606 $aComputer logic 606 $aProgramming languages (Electronic computers) 606 $aArtificial intelligence 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aSoftware Engineering/Programming and Operating Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I14002 606 $aTheory of Computation$3https://scigraph.springernature.com/ontologies/product-market-codes/I16005 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aProgramming Languages, Compilers, Interpreters$3https://scigraph.springernature.com/ontologies/product-market-codes/I14037 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 615 0$aMathematical logic. 615 0$aSoftware engineering. 615 0$aComputers. 615 0$aComputer logic. 615 0$aProgramming languages (Electronic computers). 615 0$aArtificial intelligence. 615 14$aMathematical Logic and Formal Languages. 615 24$aSoftware Engineering/Programming and Operating Systems. 615 24$aTheory of Computation. 615 24$aLogics and Meanings of Programs. 615 24$aProgramming Languages, Compilers, Interpreters. 615 24$aArtificial Intelligence. 676 $a511.3/0285 702 $aBerardi$b Stefano$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aCoppo$b Mario$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aTYPES '95 906 $aBOOK 912 $a996465861103316 996 $aTypes for Proofs and Programs$9771867 997 $aUNISA