Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








Author, Editor

Author(s):

Prevosto, Virgile
Boulmé, Sylvain

dblp
dblp

Not MPG Author(s):

Boulmé, Sylvain

Editor(s):

Urzyczyn, Pawe{ł}

dblp

Not MPII Editor(s):

Urzyczyn, Pawe{ł}

BibTeX cite key*:

PrevostoTLCA2005

Title, Booktitle

Title*:

Proof Contexts with Late Binding

Booktitle*:

Typed Lambda Calculi and Applications: 7th International Conference, TLCA 2005

Event, URLs

URL of the conference:

http://www.kurims.kyoto-u.ac.jp/rdp05/tlca/

URL for downloading the paper:


Event Address*:

Nara, Japan

Language:

English

Event Date*
(no longer used):


Organization:


Event Start Date:

21 April 2005

Event End Date:

23 April 2005

Publisher

Name*:

Springer

URL:


Address*:

Berlin, Germany

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Computer Science

Volume:

3461

Number:


Month:

April

Pages:

325-339

Year*:

2005

VG Wort Pages:


ISBN/ISSN:

3-540-25593-1

Sequence Number:


DOI:




Note, Abstract, ©

Note:

To appear

(LaTeX) Abstract:

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.



Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Programming Logics Group

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, CCL bibliography, VG Wort



BibTeX Entry:

@INPROCEEDINGS{PrevostoTLCA2005,
AUTHOR = {Prevosto, Virgile and Boulm{\'e}, Sylvain},
EDITOR = {Urzyczyn, Pawe{ł}},
TITLE = {Proof Contexts with Late Binding},
BOOKTITLE = {Typed Lambda Calculi and Applications: 7th International Conference, TLCA 2005},
PUBLISHER = {Springer},
YEAR = {2005},
VOLUME = {3461},
PAGES = {325--339},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Nara, Japan},
MONTH = {April},
ISBN = {3-540-25593-1},
NOTE = {To appear},
}


Entry last modified by Christine Kiesel, 01/28/2008
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Virgile Prevosto
Created
03/07/2005 04:19:59 PM
Revision
1.
0.


Editor
Christine Kiesel
Virgile Prevosto


Edit Date
27.04.2005 10:22:11
07/03/2005 16:19:59


Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section