A language-based approach to functionally correct imperative programming
- 12 September 2005
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 40 (9), 268-279
- https://doi.org/10.1145/1090189.1086400
Abstract
No abstract availableThis publication has 17 references indexed in Scilit:
- Combining programming with theorem provingPublished by Association for Computing Machinery (ACM) ,2005
- Safe Programming with Pointers Through Stateful ViewsLecture Notes in Computer Science, 2005
- On equivalence and canonical forms in the LF type theoryACM Transactions on Computational Logic, 2005
- The view from the leftJournal of Functional Programming, 2004
- Dependent types ensure partial correctness of theorem proversJournal of Functional Programming, 2004
- A Coverage Checking Algorithm for LFLecture Notes in Computer Science, 2003
- Proving Pointer Programs in Higher-Order LogicLecture Notes in Computer Science, 2003
- Dependently Typed Records in Type TheoryFormal Aspects of Computing, 2002
- A framework for defining logicsJournal of the ACM, 1993
- The calculus of constructionsInformation and Computation, 1988