MEMOCODE
2003
IEEE
14 years 4 months ago
2003
IEEE
An executable computational logic can provide the desired bridge between formal system properties and formal methods to verify them on the one hand, and executable models of syste...
TYPES
2004
Springer
14 years 4 months ago
2004
Springer
TYPES
2004
Springer
14 years 4 months ago
2004
Springer
Abstract Within a framework of correct code-generation from HOLspecifications, we present a particular instance concerned with the optimized compilation of a lazy language (called...
TYPES
2004
Springer
14 years 4 months ago
2004
Springer
We present four constructions for standard equipment which can be generated for every inductive datatype: case analysis, structural recursion, no confusion, acyclicity. Our constru...
TYPES
2004
Springer
14 years 4 months ago
2004
Springer
TYPES
2004
Springer
14 years 4 months ago
2004
Springer
TYPES
2004
Springer
14 years 4 months ago
2004
Springer
We present a formalization of a constructive proof of weak normalization for the simply-typed λ-calculus in the theorem prover Isabelle/HOL, and show how a program can be extracte...
TYPES
2004
Springer
14 years 4 months ago
2004
Springer
Abstract. Most approaches to the formal analysis of cryptography protocols make the perfect cryptographic assumption, which entails for example that there is no way to obtain knowl...
TYPES
2004
Springer
14 years 4 months ago
2004
Springer
Abstract. The prototype of a content based search engine for mathematical knowledge supporting a small set of queries requiring matching and/or typing operations is described. The ...
TYPES
2004
Springer
14 years 4 months ago
2004
Springer
In this paper we use the Epigram language to define the universe of regular tree types—closed under empty, unit, sum, product and least fixpoint. We then present a generic deci...