The Synthesis of a Java Card Tokenization Algorithm

DOI 10.1109/ase.2001.989789 dblp

Abstract

We describe the development of a Java bytecode optimisation algorithm by the methodology of program extraction. We develop the algorithm as a collection of proofs and definitions in the Coq proof assistant, and then use Coq's extraction mechanism to automatically generate a program in OCaml. The extraction methodology guarantees that this program is correct. We discuss the feasibility of the methodology and suggest some improvements that could be made.

BibTeX

@inproceedings{Denney:ASE01,
  author    = {Ewen Denney},
  title     = {The Synthesis of a Java Card Tokenization Algorithm},
  booktitle = {ASE},
  pages     = {43--50},
  publisher = {{IEEE} Computer Society},
  year      = {2001},
}

The Synthesis of a Java Card Tokenization Algorithm

Abstract

Related papers