CORR
2012
Springer
12 years 7 months ago
2012
Springer
The paper describes the refinement algorithm for the Calculus of (Co)Inductive Constructions (CIC) implemented in the interactive theorem prover Matita. The refinement algorithm ...
CPP
2011
12 years 11 months ago
2011
Abstract. In this paper we present a new technique for automatically verifying typing constraints in the setting of Dminor, a first-order data processing language with refinement...
JANCL
2006
13 years 11 months ago
2006
We describe KAT-ML, an implementation of an interactive theorem prover for Kleene algebra with tests (KAT). The system is designed to reflect the natural style of reasoning with K...
ACSAC
1996
IEEE
14 years 3 months ago
1996
IEEE
In this paper we describe the method used to develop a gateway capable of meeting the ITSEC E4 requirements. The security policy was formally modelled and proven consistent with t...
TPHOL
2008
IEEE
14 years 5 months ago
2008
IEEE
We describe a tutorial that demonstrates the use of the ACL2 theorem prover. We have three goals: to enable a motivated reader to start on a path towards effective use of ACL2; to...
ICFP
2008
ACM
14 years 11 months ago
2008
ACM
In the context of program verification in an interactive theorem prover, we study the problem of transforming function definitions with ML-style (possibly overlapping) pattern mat...