CATS
2006
13 years 6 months ago
2006
An O(n log n)
CATS
2006
13 years 6 months ago
2006
In this paper, we study the formalization of one-pass call-by-value CPS compilation using higher-order abstract syntax. In particular, we verify mechanically that the source progr...
CATS
2006
13 years 6 months ago
2006
CATS
2006
13 years 6 months ago
2006
The busy beaver is an example of a function which is not computable. It is based on a particular class of Turing machines, and is defined as the largest number of 1's that ca...
CATS
2006
13 years 6 months ago
2006
A complete description and proof of correctness are given for a new polynomial time algorithm for a class of codes based on directed graphs and involving construction well known i...
CATS
2006
13 years 6 months ago
2006
This paper gives an overview of a pilot project on the specification and verification of the L4 highperformance microkernel. Of the three aspects examined in the project, we descr...