Types for Proofs and Programs
Editat de Stefano Berardi, Mario Coppo, Ferruccio Damianien Limba Engleză Paperback – 15 iun 2004
Preț: 328.49 lei
Preț vechi: 410.62 lei
-20%
Puncte Express: 493
Carte tipărită la comandă
Livrare economică 27 iulie-10 august
Livrare prin curier în România Termenul estimat este afișat lângă disponibilitate.
Transport gratuit de la 400.00 lei Plată online sau ramburs, în funcție de opțiunile comenzii.
Retur gratuit în 14 zile Comandă securizată și suport în română.
Specificații
ISBN-13: 9783540221647
ISBN-10: 3540221646
Pagini: 424
Ilustrații: X, 412 p.
Dimensiuni: 155 x 235 x 23 mm
Greutate: 0.64 kg
Ediția:2004
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
ISBN-10: 3540221646
Pagini: 424
Ilustrații: X, 412 p.
Dimensiuni: 155 x 235 x 23 mm
Greutate: 0.64 kg
Ediția:2004
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
Public țintă
ResearchCuprins
A Modular Hierarchy of Logical Frameworks.- Tailoring Filter Models.- Locales and Locale Expressions in Isabelle/Isar.- to PAF!, a Proof Assistant for ML Programs Verification.- A Constructive Proof of Higman’s Lemma in Isabelle.- A Core Calculus of Higher-Order Mixins and Classes.- Type Inference for Nested Self Types.- Inductive Families Need Not Store Their Indices.- Modules in Coq Are and Will Be Correct.- Rewriting Calculus with Fixpoints: Untyped and First-Order Systems.- First-Order Reasoning in the Calculus of Inductive Constructions.- Higher-Order Linear Ramified Recurrence.- Confluence and Strong Normalisation of the Generalised Multiary ?-Calculus.- Wellfounded Trees and Dependent Polynomial Functors.- Classical Proofs, Typed Processes, and Intersection Types.- “Wave-Style” Geometry of Interaction Models in Rel Are Graph-Like Lambda-Models.- Coercions in Hindley-Milner Systems.- Combining Incoherent Coercions for ? -Types.- Induction and Co-induction in Sequent Calculus.- QArith: Coq Formalisation of Lazy Rational Arithmetic.- Mobility Types in Coq.- Some Algebraic Structures in Lambda-Calculus with Inductive Types.- A Concurrent Logical Framework: The Propositional Fragment.- Formal Proof Sketches.- Applied Type System.