• Implementation
    • Worked intensively with language-based syntactic editor CSG (Cornell Synthesizer Generator) and unix tools Yacc and Lex.
    • Worked intensively with functional langauges (like PAnndAS and SML) for implementing source-to-soruce translators and transformations.
    • Proposed in the thesis parameterized presentation for logical frameworks
    • System Integration and Maintanence in PROSPECTRA project
  • Working Expierence with exsited systems
    • PROSPECTRA
    • LEGO (proof checker based on type theory)
    • ISABELLE (proof development based on higher-order unification)
    • KIV (Kalsruhe Interactive verifier for program verification)
    • DaVinci (Graph Visualization) visualizing development graph