Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
  Proof Contexts with Late Binding

Prevosto, V., & Boulmé, S. (2005). Proof Contexts with Late Binding. In Typed Lambda Calculi and Applications: 7th International Conference, TLCA 2005 (pp. 325-339). Berlin, Germany: Springer.

Item is

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Prevosto, Virgile1, Autor           
Boulmé, Sylvain, Autor
Urzyczyn, Pawe{l}, Herausgeber
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: The focal language (formerly Foc) allows one to incrementally build modules and to prove formally their correctness. focal encourages a development process by refinement, deriving step-by-step implementations from specifications. This refinement process is realized using an inheritance mechanism on structures which can mix primitive operations, axioms, algorithms and proofs. Inheriting from existing structures allows to reuse their components under some conditions, statically checked by the compiler. This paper presents two formal semantics for encoding focal constructions in the Coq proof assistant. The first one is a shallow embedding which gives a practical way to use Coq to check proofs in focal libraries. The second one formalizes the focal structures as Coq types (called mixDrecs) and shows that the informal semantics of focal libraries is coherent with respect to Coq logic. In the last part of the paper, we prove that the first embedding is conform to the mixDrecs model.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2005-04-272005
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 279115
Anderer: Local-ID: C1256104005ECAFC-FD4A77D3E010E4C8C1256FBD00543A20-PrevostoTLCA2005
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: Untitled Event
Veranstaltungsort: Nara, Japan
Start-/Enddatum: 2005-04-21

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Typed Lambda Calculi and Applications: 7th International Conference, TLCA 2005
Genre der Quelle: Konferenzband
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: Berlin, Germany : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 325 - 339 Identifikator: ISBN: 3-540-25593-1

Quelle 2

einblenden:
ausblenden:
Titel: Lecture Notes in Computer Science
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 3461 Artikelnummer: - Start- / Endseite: - Identifikator: -