papers

Michael Lampis, Kyriakos G. Ginis, Michalis A. Papakyriakou, Nikolaos S. Papaspyrou.
Quantum data and control made easier
In Electronic Notes in Theoretical Computer Science, Volume 210, 11 July 2008, Pages 85-105

pdf… abstract… sources…

Angelos Manousaridis, Michalis Papakyriakou and Nikolaos Papaspyrou.
From Program Verification to Certified Binaries
In Computability in Europe 2008, June 2008

pdf… slides… sources…

Michalis A. Papakyriakou and Nikolaos S. Papaspyrou.
Mechanized Proofs of Type Safety for a Family of Lambda Calculi with References
In 2nd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory, October 2007

pdf… slides… slides (long version)… sources…

Michalis A. Papakyriakou, Prodromos E. Gerakios and Nikolaos S. Papaspyrou.
A Mechanized Proof of Type Safety for the Polymorphic Lambda Calculus with References
In 6th Panhellenic Logic Symposium, July 2007

pdf… slides… abstract… sources…

Nikolaos S. Papaspyrou, Michalis A. Papakyriakou and Angelos Manousaridis.
Encoding Hoare Logic in Typed Certified Code
In 5th Panhellenic Logic Symposium, June 2005

pdf… slides… abstract… sources…

pending

Michalis A. Papakyriakou and Nikolaos S. Papaspyrou.
From Linear to Unrestricted and Back: Type Safety and the Let-bang Construct

sources…

under-grad projects

A compiler for a simple c-like language, using flex/bison, which produces MASM like ASM.
Co-worker: Theodoros Tsokos

web page (in Greek)… source code…