1
Preface
Philippe Audebaud,
Christine Paulin-Mohring
March 2011
Science of Computer Programming: Volume 76 Issue 3, March, 2011
Publisher: Elsevier North-Holland, Inc.
2
Proofs of randomized algorithms in Coq
Philippe Audebaud,
Christine Paulin-Mohring
June 2009
Science of Computer Programming: Volume 74 Issue 8, June, 2009
Publisher: Elsevier North-Holland, Inc.
Randomized algorithms are widely used for finding efficiently approximated solutions to complex problems, for instance primality testing and for obtaining good average behavior. Proving properties of such algorithms requires subtle reasoning both on algorithmic and probabilistic aspects of programs. Thus, providing tools for the mechanization of reasoning is an important ...
Keywords:
Functional language, Monadic interpretation, Probability framing, Randomized algorithms, Axiomatic semantics, Call-by-value, Proof of partial and total correctness
3
Proofs of randomized algorithms in CoQ
Philippe Audebaud,
Christine Paulin-Mohring
July 2006
MPC'06: Proceedings of the 8th international conference on Mathematics of Program Construction
Publisher: Springer-Verlag
Randomized algorithms are widely used either for finding efficiently approximated solutions to complex problems, for instance primality testing, or for obtaining good average behavior, for instance in distributed computing. Proving properties of such algorithms requires subtle reasoning both on algorithmic and probabilistic aspects of the programs. Providing tools for the ...
4
Types for Proofs and Programs: International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers (Lecture Notes in Computer Science)
Jean-Christophe Filliatre,
Christine Paulin-Mohring,
Benjamin Werner
March 2006
5
Reasoning about java programs with aliasing and frame conditions
Claude Marché,
Christine Paulin-Mohring
August 2005
TPHOLs'05: Proceedings of the 18th international conference on Theorem Proving in Higher Order Logics
Publisher: Springer-Verlag
Several tools exist for reasoning about Java programs annotated with JML specifications. A main issue is to deal with possible aliasing between objects and to handle correctly the frame conditions limiting the part of memory that a method is allowed to modify. Tools designed for automatic use (like ESC/Java) are ...
6
Formal verification of security properties of smart card embedded source code
June Andronick,
Boutheina Chetali,
Christine Paulin-Mohring
July 2005
FM'05: Proceedings of the 2005 international conference on Formal Methods
Publisher: Springer-Verlag
This paper reports on a method to handle the verification of various security properties of imperative source code embedded on smart cards. The idea is to combine two program verification approaches: the functional verification at the source code level and the verification of high level properties on a formal model ...
Keywords:
source code verification, theorem proving, formal methods, security, smart card
7
Modelisation of Timed Automata in Coq
Christine Paulin-Mohring
October 2001
TACS '01: Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software
Publisher: Springer-Verlag
This paper presents the modelisation of a special class of timed automata, named p-automata in the proof assistant Coq. This work was performed in the framework of the CALIFE project1 which aims to build a general platform for specification, validation and test of critical algorithms involved in telecommunications. This paper ...
8
Introduction
Eduardo Giménez,
Christine Paulin-Mohring
December 1996
TYPES '96: Selected papers from the International Workshop on Types for Proofs and Programs
Publisher: Springer-Verlag
9
Circuits as Streams in Coq: Verification of a Sequential Multiplier
Christine Paulin-Mohring
June 1995
TYPES '95: Selected papers from the International Workshop on Types for Proofs and Programs
Publisher: Springer-Verlag
10
Programming with streams in Coq: a case study: the Sieve of Eratosthenes
François Leclerc,
Christine Paulin-Mohring
January 1994
TYPES '93: Proceedings of the international workshop on Types for proofs and programs
Publisher: Springer-Verlag New York, Inc.
11
Synthesis of ML programs in the system Coq
Christine Paulin-Mohring,
Benjamin Werner
May 1993
Journal of Symbolic Computation - Special issue on automatic programming: Volume 15 Issue 5-6, May/June 1993
Publisher: Academic Press, Inc.
The system Coq (Dowek et al., 1991) is an environment for proof development based on the Calculus of Constructions (Coquand, 1985) (Coquand and Huet, 1985) enhanced with inductive definitions (Coquand and Paulin-Mohring, 1990). From a constructive proof formalized in Coq, one extracts a functional program which can be compiled and ...
12
Inductive Definitions in the system Coq - Rules and Properties
Christine Paulin-Mohring
March 1993
TLCA '93: Proceedings of the International Conference on Typed Lambda Calculi and Applications
Publisher: Springer-Verlag
13
Inductively defined types in the calculus of constructions
July 1990
Proceedings of the fifth international conference on Mathematical foundations of programming semantics
Publisher: Springer-Verlag New York, Inc.
14
Inductively Defined Types in the Calculus of Constructions
March 1989
Proceedings of the 5th International Conference on Mathematical Foundations of Programming Semantics
Publisher: Springer-Verlag
15
Extracting Ω's programs from proofs in the calculus of constructions
C. Paulin-Mohring
January 1989
POPL '89: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages
Publisher: ACM
Bibliometrics:
Citation Count: 37
Downloads (6 Weeks): 7, Downloads (12 Months): 19, Downloads (Overall): 294
Full text available:
PDF
We define in this paper a notion of realizability for the Calculus of Constructions. The extracted programs are terms of the Calculus that do not contain dependent types. We introduce a distinction between informative and non-informative propositions. This distinction allows the removal of the “logical” part in the development of ...
Author only
