ESOP
2010
Springer
13 years 12 months ago
2010
Springer
Parsing is an important problem in computer science and yet surprisingly little attention has been devoted to its formal verification. In this paper, we present TRX: a parser inter...
TPHOL
1999
IEEE
14 years 24 days ago
1999
IEEE
We present a development of Universal Algebra inside Type Theory, formalized using the proof assistant Coq. We define the notion of a signature and of an algebra over a signature. ...
TPHOL
2002
IEEE
14 years 1 months ago
2002
IEEE
Abstract. This paper describes a formalization of the weakest precondition, wp, for general recursive programs using the type-theoretical proof assistant Coq. The formalization is ...
SAC
2006
ACM
14 years 2 months ago
2006
ACM
We provide sufficient conditions that formally guarantee that the floating-point computation of a polynomial evaluation is faithful. To this end, we develop a formalization of ...
ICICS
2007
Springer
14 years 2 months ago
2007
Springer
Abstract. To be accepted, a cryptographic scheme must come with a proof that it satisfies some standard security properties. However, because cryptographic schemes are based on no...