602 search results - page 1 / 121 » Program Calculation in Coq |
AMAST
2010
Springer
12 years 12 months ago
2010
Springer
ENTCS
2008
13 years 4 months ago
2008
This paper presents fixpoint calculations on lattice structures as example of highly modular programming in a dependently typed functional language. We propose a library of Coq mo...
CIE
2008
Springer
13 years 6 months ago
2008
Springer
The extraction mechanism of Coq allows one to transform Coq proofs and functions into functional programs. We illustrate the behavior of this tool by reviewing several variants of ...
IPPS
2002
IEEE
13 years 9 months ago
2002
IEEE
We present a formalization of a proof of self-stabilization in the Coq proof assistant. Coq is a program allowing to define mathematical objects and properties, and to make proof...
TPHOL
2009
IEEE
13 years 11 months ago
2009
IEEE
Abstract. This pearl examines how to verify functional programs written using the state monad. It uses Coq’s Program framework to provide strong specifications for the standard ...