POPL
2012
ACM
12 years 7 months ago
2012
ACM
Differential privacy is a notion of confidentiality that protects the privacy of individuals while allowing useful computations on their private data. Deriving differential priva...
FORTE
2011
13 years 3 months ago
2011
Abstract. Data centric languages, such as recursive rule based languages, have been proposed to program distributed applications over networks. They simplify greatly the code, whic...
ISSE
2010
13 years 6 months ago
2010
In this work, we address the formalisation of symmetric nets, a subclass of coloured Petri nets, refinement in COQ. We first provide a formalisation of the net models, and of thei...
ENTCS
2002
13 years 11 months ago
2002
We describe a proof dedicated meta-language, called Ltac, in the context of the Coq proof assistant. This new layer of meta-language is quite appropriate to write small and local ...
JAR
2008
13 years 11 months ago
2008
This article presents the formal verification, using the Coq proof assistant, of a memory model for low-level imperative languages such as C and compiler intermediate languages. Be...
ENTCS
2006
13 years 12 months ago
2006
It is a well-known fact that algorithms are often hidden inside mathematical proofs. If these proofs are formalized inside a proof assistant, then a mechanism called extraction ca...
FOSSACS
2008
Springer
14 years 1 months ago
2008
Springer
Abstract. In this paper, we show how Miquel's Implicit Calculus of Constructions (ICC) can be used as a programming language featuring dependent types. Since this system has a...
TYPES
2000
Springer
14 years 3 months ago
2000
Springer
We describe a construction of the real numbers carried out in the Coq proof assistant. The basis is a set of axioms for the constructive real numbers as used in the FTA (Fundamenta...
FM
2006
Springer
14 years 3 months ago
2006
Springer
This paper presents the formal verification of a compiler front-end that translates a subset of the C language into the Cminor intermediate language. The semantics of the source an...
FLOPS
2006
Springer
14 years 3 months ago
2006
Springer
Abstract. We present a practical tool for defining and proving properties of recursive functions in the Coq proof assistant. The tool generates from pseudo-code the graph of the in...