Types for Proofs and Programs International Conference, TYPES 2008 Torino, Italy, March 26-29, 2008 Revised Selected Papers /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Berardi, Stefano (Επιμελητής έκδοσης), Damiani, Ferruccio (Επιμελητής έκδοσης), de’Liguoro, Ugo (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2009.
• Σειρά: Lecture Notes in Computer Science, 5497
• Θέματα: Computer science.; Computer programming.; Programming languages (Electronic computers).; Computer logic.; Mathematical logic.; Computer science > Mathematics.; Artificial intelligence.; Computer Science.; Programming Techniques.; Logics and Meanings of Programs.; Mathematical Logic and Formal Languages.; Programming Languages, Compilers, Interpreters.; Symbolic and Algebraic Manipulation.; Artificial Intelligence (incl. Robotics).

This 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 we...

Πίνακας περιεχομένων:

• Type 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.