LEADER 04802nam  22008295  450 
001 996465856203316
005 20230406063102.0
010   $a3-642-02444-0
024 7 $a10.1007/978-3-642-02444-3
035   $a(CKB)1000000000754001
035   $a(SSID)ssj0000320544
035   $a(PQKBManifestationID)11258727
035   $a(PQKBTitleCode)TC0000320544
035   $a(PQKBWorkID)10249724
035   $a(PQKB)11714910
035   $a(DE-He213)978-3-642-02444-3
035   $a(MiAaPQ)EBC3064272
035   $a(PPN)136306861
035   $a(EXLCZ)991000000000754001
100   $a20100301d2009      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 Conference, TYPES 2008 Torino, Italy, March 26-29, 2008 Revised Selected Papers /$fedited by Stefano Berardi, Ferruccio Damiani, Ugo de Liguoro
205   $a1st ed. 2009.
210  1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2009.
215   $a1 online resource (VIII, 323 p.) 
225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v5497
300   $aBibliographic Level Mode of Issuance: Monograph
311   $a3-642-02443-2 
320   $aIncludes bibliographical references and author index.
327   $aType Inference by Coinductive Logic Programming -- About the Formalization of Some Results by Chebyshev in Number Theory -- A New Elimination Rule for the Calculus of Inductive Constructions -- A Framework for the Analysis of Access Control Models for Interactive Mobile Devices -- Proving Infinitary Normalization -- First-Class Object Sets -- Monadic Translation of Intuitionistic Sequent Calculus -- Towards a Type Discipline for Answer Set Programming -- Type Inference for a Polynomial Lambda Calculus -- Local Theory Specifications in Isabelle/Isar -- Axiom Directed Focusing -- A Type System for Usage of Software Components -- Merging Procedural and Declarative Proof -- Using Structural Recursion for Corecursion -- Manifest Fields and Module Mechanisms in Intensional Type Theory -- A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq -- Coalgebraic Reasoning in Coq: Bisimulation and the ?-Coiteration Scheme -- A Process-Model for Linear Programs -- Some Complexity and Expressiveness Results on Multimodal and Stratified Proof Nets.
330   $aThis book constitutes the thoroughly refereed post-conference proceedings of TYPES 2008, the last of a series of meetings of the TYPES working group funded by the European Union between 1993 and 2008; the workshop has been held in Torino, Italy, in March 2008. The 19 revised full papers presented were carefully reviewed and selected from 27 submissions. The topic of the workshop was formal reasoning and computer programming based on type theory: languages and computerized tools for reasoning, and applications in several domains such as analysis of programming languages, certified software, mobile code, formalization of mathematics, mathematics education.
410  0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v5497
606   $aComputer programming
606   $aComputer science
606   $aMachine theory
606   $aCompilers (Computer programs)
606   $aComputer science?Mathematics
606   $aArtificial intelligence
606   $aProgramming Techniques
606   $aComputer Science Logic and Foundations of Programming
606   $aFormal Languages and Automata Theory
606   $aCompilers and Interpreters
606   $aSymbolic and Algebraic Manipulation
606   $aArtificial Intelligence
615  0$aComputer programming.
615  0$aComputer science.
615  0$aMachine theory.
615  0$aCompilers (Computer programs).
615  0$aComputer science?Mathematics.
615  0$aArtificial intelligence.
615 14$aProgramming Techniques.
615 24$aComputer Science Logic and Foundations of Programming.
615 24$aFormal Languages and Automata Theory.
615 24$aCompilers and Interpreters.
615 24$aSymbolic and Algebraic Manipulation.
615 24$aArtificial Intelligence.
676   $a005.13122gerDNB
686   $aDAT 373f$2stub
686   $aDAT 510f$2stub
686   $aDAT 706f$2stub
686   $aSS 4800$2rvk
702   $aBerardi$b Stefano$4edt$4http://id.loc.gov/vocabulary/relators/edt
702   $aDamiani$b Ferruccio$4edt$4http://id.loc.gov/vocabulary/relators/edt
702   $ade Liguoro$b Ugo$4edt$4http://id.loc.gov/vocabulary/relators/edt
906   $aBOOK
912   $a996465856203316
996   $aTypes for Proofs and Programs$9771867
997   $aUNISA