Learning how to Prove: From the Coq Proof Assistant to Textbook Style
We have developed an alternative approach to teaching computer science students how to prove. First, students are taught how to prove theorems with the Coq proof assistant. In a second, more difficult, step students will transfer their acquired skills to the area of textbook proofs. In this article...
Main Authors: | Sebastian Böhne, Christoph Kreitz |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2018-03-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1803.01466v1 |
Similar Items
-
CoqIOA : a formalization of IO automata in the Coq proof assistant
by: Athalye, Anish (Anish R.)
Published: (2017) -
Formally Verified Code Obfuscation in the Coq Proof Assistant
by: Lu, Weiyun
Published: (2019) -
An Introduction to Programming and Proving with Dependent Types in Coq
by: Adam Chlipala
Published: (2010-01-01) -
jsCoq: Towards Hybrid Theorem Proving Interfaces
by: Emilio Jesús Gallego Arias, et al.
Published: (2017-01-01) -
Formal Proof of a Machine Closed Theorem in Coq
by: Hai Wan, et al.
Published: (2014-01-01)