Types for Proofs and Programs
Editat de Stefano Berardi, Mario Coppo, Ferruccio Damianien Limba Engleză Paperback – 15 iun 2004
Preț: 327.49 lei
Preț vechi: 409.37 lei
-20% Nou
Puncte Express: 491
Preț estimativ în valută:
57.95€ • 67.58$ • 50.88£
57.95€ • 67.58$ • 50.88£
Carte tipărită la comandă
Livrare economică 16-30 ianuarie 26
Preluare comenzi: 021 569.72.76
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.
Caracteristici
Includes supplementary material: sn.pub/extras