Types for Proofs and Programs
Springer Berlin (Hersteller)
978-3-540-48440-0 (ISBN)
Proving strong normalization of CC by modifying realizability semantics.- Checking algorithms for Pure Type Systems.- Infinite objects in type theory.- Conservativity between logics and typed ? calculi.- Logic of refinement types.- Proof-checking a data link protocol.- Elimination of extensionality in Martin-Löf type theory.- Programming with streams in Coq a case study: The Sieve of Eratosthenes.- The Alf proof editor and its proof engine.- Encoding Z-style Schemas in type theory.- The expressive power of Structural Operational Semantics with explicit assumptions.- Developing certified programs in the system Coq the program tactic.- Closure under alpha-conversion.- Machine Deduction.- Type theory and the informal language of mathematics.- Semantics for abstract clauses.
| Erscheint lt. Verlag | 6.7.2005 |
|---|---|
| Reihe/Serie | Computer Science |
| Computer Science (R0) | Lecture Notes in Computer Science |
| Zusatzinfo | IX, 395 p. |
| Verlagsort | Berlin |
| Sprache | englisch |
| Themenwelt | Mathematik / Informatik ► Informatik ► Software Entwicklung |
| Informatik ► Theorie / Studium ► Künstliche Intelligenz / Robotik | |
| Schlagworte | Databases • Lambda-Calculus • linear optimization • logical reasoning • Machine Deduction • Maschinelles Schließen • proof checking • theorem proving • Typentheorie • Types |
| ISBN-10 | 3-540-48440-X / 354048440X |
| ISBN-13 | 978-3-540-48440-0 / 9783540484400 |
| Zustand | Neuware |
| Informationen gemäß Produktsicherheitsverordnung (GPSR) | |
| Haben Sie eine Frage zum Produkt? |
