Towards Formal Proof Script Refactoring
From MaRDI portal
Publication:5200123
DOI10.1007/978-3-642-22673-1_18zbMath1335.68240OpenAlexW2195779287MaRDI QIDQ5200123
Lucas Dixon, Iain Whiteside, Gudmund Grov, David Aspinall
Publication date: 29 July 2011
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://www.pure.ed.ac.uk/ws/files/17654842/RefactoringProof.pdf
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (3)
Aligning concepts across proof assistant libraries ⋮ CoqPIE: An IDE Aimed at Improving Proof Development Productivity ⋮ Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
Uses Software
Cites Work
- Tactics for hierarchical proof
- Presenting and Explaining Mizar
- Proof Transformations for Evolutionary Formal Software Development
- A Declarative Language for the Coq Proof Assistant
- The Four Colour Theorem: Engineering of a Formal Proof
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Towards Formal Proof Script Refactoring
