Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

15

TLCA
2005
Springer

favoriteEmaildiscussreport

127views Theoretical Computer Science» more TLCA 2005»

Proof Contexts with Late Binding

13 years 10 months ago

Proof Contexts with Late Binding

Download focal.inria.fr

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 ﬁrst one is implemented in the Focal compiler to have the correctness of Focal libraries veriﬁed 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.

Virgile Prevosto, Sylvain Boulmé

Real-time Traffic

Coq Proof Assistant | Focal | Focal Language | Theoretical Computer Science | TLCA 2005 |

claim paper

Related Content

» Activityoriented contextaware adaptation assisting mobile geospatial activities

» StrongAspectJ flexible and safe pointcutadvice bindings

» A Basic Model of Typed Components

» Managing NonFunctional Properties of Interenterprise Business Service Delivery

» Generic Wrappers

» Named Models in Coalgebraic Hybrid Logic

» Combining generic judgments with recursive definitions

» Resolving Inductive Definitions with Binders in HigherOrder Typed Functional Programming

» Model Checking for Nominal Calculi

Post Info
More Details (n/a)

Added	28 Jun 2010
Updated	28 Jun 2010
Type	Conference
Year	2005
Where	TLCA
Authors	Virgile Prevosto, Sylvain Boulmé

Comments (0)