IntelliSense Integration for Coq Theorem Prover
| Název práce v češtině: | IntelliSense Integration for Coq Theorem Prover |
|---|---|
| Název v anglickém jazyce: | IntelliSense Integration for Coq Theorem Prover |
| Akademický rok vypsání: | 2009/2010 |
| Typ práce: | diplomová práce |
| Jazyk práce: | angličtina |
| Ústav: | Katedra softwarového inženýrství (32-KSI) |
| Vedoucí / školitel: | Mgr. Tomáš Petříček, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 09.09.2010 |
| Datum zadání: | 09.09.2010 |
| Datum potvrzení stud. oddělením: | 01.08.2011 |
| Datum a čas obhajoby: | 28.05.2012 10:30 |
| Datum odevzdání elektronické podoby: | 13.04.2012 |
| Datum odevzdání tištěné podoby: | 13.04.2012 |
| Datum proběhlé obhajoby: | 28.05.2012 |
| Oponenti: | RNDr. David Bednárek, Ph.D. |
| Zásady pro vypracování |
| The goal of this work is to design and implement Visual Studio 2010 IntelliSense integration for the language used in the Coq theorem prover. Coq is a system for interactive development and formalization of mathematical proofs. The integration should simplify both proof writing as well as interactive verification of the proof.
The key components of the work are syntax highlighting for the language used in Coq (using standard lexical analysis tools), autocompletion of identificators and language keywords (Coq recognizes names of prepositions, types and type constructors that should be suggested based on the semantic analysis) and an interactive goal window for displaying the immediate proof state. |
| Seznam odborné literatury |
| [1] B. Barras et al. The Coq Proof Assistant reference manual. Technical report, INRIA, 1998.
[2] Microsoft. Visual Studio 2010 Integration SDK. Online at: http://msdn.microsoft.com/en-us/library/bb165336.aspx [3] The Coq Development Team. Coq Integrated Development Environment. Online at: http://coq.inria.fr/V8.1/refman/Reference-Manual016.html [4] G. Little and R. C. Miller. Keyword programming in java. In Proceedings of ASE 2007, pages 84?93, 2007. [5] G. Murphy, M. Kersten, and L. Findlater. How are java software developers using the eclipse ide? IEEE Software, jul 2006. [6] A. V. Aho, R. Sethi, J. D. Ullman: Compilers: Principles, Techniques, and Tools. Addison-Wesley 1986 [7] A. Chlipala: Certified Programming with Dependent Types (Draft). Online at: http://adam.chlipala.net/cpdt/ [8] Y. Bertot, P. Castéran: Interactive Theorem Proving and Program Development. Springer, 2004 [9] H. Goguen, P. Loiseleur, D. Aspinall, P. Courtieu: Coq Proof General for Coq. Online at: http://proofgeneral.inf.ed.ac.uk/ |