Proof contexts with late binding

Virgile Prevosto; Sylvain Boulmé

doi:10.1007/11417170_24

Proof contexts with late binding

Virgile Prevosto
, Sylvain Boulmé

Max-Planck-Institut fur Informatik
LSR-IMAG

Research output: Contribution to journal › Conference article › peer-review

3 Citations (Scopus)

Abstract

The FOCAL language (formerly FoC) allows one to incrementally build modules and to formally prove their correctness. In this paper, we present two formal semantics for encoding FOCAL constructions in the COQ proof assistant. The first one is implemented in the FOCAL compiler to have the correctness of FOCAL libraries verified with the COQ proof-checker. The second one formalizes the FOCAL structures and their main properties as COQ terms (called mixDrecs). The relations between the two embeddings are examined in the last part of the paper.

Original language	English
Pages (from-to)	324-338
Number of pages	15
Journal	Lecture Notes in Computer Science
Volume	3461
DOIs	https://doi.org/10.1007/11417170_24
Publication status	Published - 1 Jan 2005
Externally published	Yes
Event	7th International Conference on Typed Lambda Calculi and Applications, TLCA 2005 - Nara, Japan Duration: 21 Apr 2005 → 23 Apr 2005

Access to Document

10.1007/11417170_24

Cite this

@article{fe16bbcebeec4320bf0b1a597b6aaea8,

title = "Proof contexts with late binding",

abstract = "The FOCAL language (formerly FoC) allows one to incrementally build modules and to formally prove their correctness. In this paper, we present two formal semantics for encoding FOCAL constructions in the COQ proof assistant. The first one is implemented in the FOCAL compiler to have the correctness of FOCAL libraries verified with the COQ proof-checker. The second one formalizes the FOCAL structures and their main properties as COQ terms (called mixDrecs). The relations between the two embeddings are examined in the last part of the paper.",

author = "Virgile Prevosto and Sylvain Boulm{\'e}",

year = "2005",

month = jan,

day = "1",

doi = "10.1007/11417170\_24",

language = "English",

volume = "3461",

pages = "324--338",

journal = "Lecture Notes in Computer Science",

issn = "0302-9743",

note = "7th International Conference on Typed Lambda Calculi and Applications, TLCA 2005 ; Conference date: 21-04-2005 Through 23-04-2005",

}

TY - JOUR

T1 - Proof contexts with late binding

AU - Prevosto, Virgile

AU - Boulmé, Sylvain

PY - 2005/1/1

Y1 - 2005/1/1

N2 - The FOCAL language (formerly FoC) allows one to incrementally build modules and to formally prove their correctness. In this paper, we present two formal semantics for encoding FOCAL constructions in the COQ proof assistant. The first one is implemented in the FOCAL compiler to have the correctness of FOCAL libraries verified with the COQ proof-checker. The second one formalizes the FOCAL structures and their main properties as COQ terms (called mixDrecs). The relations between the two embeddings are examined in the last part of the paper.

AB - The FOCAL language (formerly FoC) allows one to incrementally build modules and to formally prove their correctness. In this paper, we present two formal semantics for encoding FOCAL constructions in the COQ proof assistant. The first one is implemented in the FOCAL compiler to have the correctness of FOCAL libraries verified with the COQ proof-checker. The second one formalizes the FOCAL structures and their main properties as COQ terms (called mixDrecs). The relations between the two embeddings are examined in the last part of the paper.

U2 - 10.1007/11417170_24

DO - 10.1007/11417170_24

M3 - Conference article

AN - SCOPUS:24944481686

SN - 0302-9743

VL - 3461

SP - 324

EP - 338

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

T2 - 7th International Conference on Typed Lambda Calculi and Applications, TLCA 2005

Y2 - 21 April 2005 through 23 April 2005

ER -

Proof contexts with late binding

Abstract

Access to Document

Fingerprint

Cite this