PPDP
2007
Springer
14 years 6 months ago
2007
Springer
We describe a semantic type soundness result, formalized in the Coq proof assistant, for a compiler from a simple imperative language with heap-allocated data into an idealized as...
TLCA
2009
Springer
14 years 6 months ago
2009
Springer
We show that, in a parametric model of polymorphism, the type ∀α.((α → α) → α) → (α → α → α) → α is isomorphic to closed n terms. That is, the type of closed ...
FROCOS
2009
Springer
14 years 6 months ago
2009
Springer
In an attempt to improve automation capabilities in the Coq proof assistant, we develop a tactic for the propositional fragment based on the DPLL procedure. Although formulas natur...
WOLLIC
2009
Springer
14 years 6 months ago
2009
Springer
We give a simple intuitionistic completeness proof of Kripke semantics with constant domain for intuitionistic logic with implication and universal quantification. We use a cut-fr...
POPL
2010
ACM
14 years 9 months ago
2010
ACM
We present a verified compiler to an idealized assembly language from a small, untyped functional language with mutable references and exceptions. The compiler is programmed in th...
ICFP
2002
ACM
15 years 1 days ago
2002
ACM
Motivated by applications to proof assistants based on dependent types, we develop and prove correct a strong reducer and equivalence checker for the -calculus with products, sums...
ICFP
2004
ACM
15 years 1 days ago
2004
ACM
Concurrency, as a useful feature of many modern programming languages and systems, is generally hard to reason about. Although existing work has explored the verification of concu...
ICFP
2006
ACM
15 years 1 days ago
2006
ACM
I report on an experience using the Coq proof assistant to develop a program verification tool with a machine-checkable proof of full correctness. The verifier is able to prove me...
ICFP
2008
ACM
15 years 1 days ago
2008
ACM
We describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects. C...
CADE
2003
Springer
15 years 12 days ago
2003
Springer
This paper presents on-going researches on theoretical and practical issues of combining rewriting based automated theorem proving and user-guided proof development, with the stron...