Merkzettel Warenkorb
  • Produktbild: Types for Proofs and Programs
  • Produktbild: Types for Proofs and Programs
Band 1158

Types for Proofs and Programs International Workshop, TYPES '95, Torino, Italy, June 5-8, 1995. Selected Papers

Aus der Reihe Lecture Notes in Computer Science

49,99 €

inkl. gesetzl. MwSt., Versandkostenfrei

Lieferung nach Hause

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

02.10.1996

Herausgeber

Stefano Berardi + weitere

Verlag

Springer Berlin

Seitenzahl

298

Maße (L/B/H)

23,5/15,5/1,6 cm

Gewicht

476 g

Auflage

1996

Sprache

Englisch

ISBN

978-3-540-61780-8

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

02.10.1996

Herausgeber

Verlag

Springer Berlin

Seitenzahl

298

Maße (L/B/H)

23,5/15,5/1,6 cm

Gewicht

476 g

Auflage

1996

Sprache

Englisch

ISBN

978-3-540-61780-8

Herstelleradresse

Springer-Verlag KG
Sachsenplatz 4-6
1201 Wien
AT

Email: GPSR Kontakt

Noch keine Bewertungen vorhanden

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kundinnen und Kunden durch Ihre Meinung.

Kundinnen und Kunden meinen

Bewertungen (0)
  • Produktbild: Types for Proofs and Programs
  • Produktbild: Types for Proofs and Programs
  • Implicit 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.