Languages and Tools

Proof Assistants and Logical Frameworks:      The Coq Proof Assistant      Isabelle/HOL      Twelf      The LEGO Proof Assistant
LaTeX:     hyperref      CTeX and CTex-fonts      The Not So Short Introduction      The Comprehensive LaTeX Symbol List      XYpic

Research Groups and Projects

Flint      Concurrent C Minor      Compcert      Singularity@MSR      Cyclone      CCured      The VeriSoft Project

Assembly Programming, OS and Device Drivers

Interfacing the PC      PIC and Interrupts      Yale CS422      Bochs      Bochs internal debugger      µC/OS-II      TinyOS      nesC      Workshop on Operating Systems Verification      L4.verified      Workshop on System Verification (SV'06)

Successful Career

Career:      "How to Have a Bad Career In Research/Academia" by David Patterson
Writing and Presentatins:
Referee:      "The Task of the Referee" by Alan Jay Smith


Merriam-Webster Online      Wikipedia
Programming Language Theory Text Online
ACM Digital Library      IEEE Xplore      Google Scholar

Xinyu Feng
Last modified: Sun Dec 17 11:39:20 EST 2006