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

Résultats de recherche: Contribution à un journal › Article de conférence › Revue par des pairs

Résumé

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.

langue originale	Anglais
Pages (de - à)	324-338
Nombre de pages	15
journal	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3461
Les DOIs	https://doi.org/10.1007/11417170_24
état	Publié - 1 janv. 2005
Modification externe	Oui
Evénement	7th International Conference on Typed Lambda Calculi and Applications, TLCA 2005 - Nara, Japon Durée: 21 avr. 2005 → 23 avr. 2005

Accès au document

10.1007/11417170_24

Contient cette citation

@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 (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

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 (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

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

Résumé

Accès au document

Empreinte digitale

Contient cette citation