• 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