Software specifications, Software/Hardware standards like RFCs, patents etc and Mathematical proofs are normally written in plain natural language. Natural languages are rich, complex, and ambiguous. Having this in mind, Formal methods try to solve this problem by replacing natural languages with rich mathematical formalisms which are understood by model checkers or theorem provers. They are very precise, accurate and clear but not easily understood by domain experts such as Software designers, programmers, engineers and Mathematicians.
This project is an attempt to make a connection between formal and natural languages. We are developing a controlled natural language having large coverage, which will be good enough for writing Software Specifications and Mathematical Proofs interactively.
We are currently working on parsing and translation of Mathematical proofs written in Natural language (English). Therefore I'll talk on Mathematical proofs for most of the time. Specifically I'll explain the implementation details.
Project homepage: http://www.lama.univ-savoie.fr/~humayoun/phd/index.html .