Skip to Main content Skip to Navigation
New interface
Conference papers

Reasoning about computations using two-levels of logic

Dale Miller 1, 2 
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : We describe an approach to using one logic to reason about specifications written in a second logic. One level of logic, called the ''reasoning logic'', is used to state theorems about computational specifications. This logic is classical or intuitionistic and should contain strong proof principles such as induction and co-induction. The second level of logic, called the ''specification logic'', is used to specify computation. While computation can be specified using a number of formal techniques---e.g., Petri nets, process calculus, and state machines---we shall illustrate the merits and challenges of using logic programming-like specifications of computation.
Document type :
Conference papers
Complete list of metadata

Cited literature [45 references]  Display  Hide  Download
Contributor : Dale Miller Connect in order to contact the contributor
Submitted on : Thursday, January 10, 2013 - 5:56:41 PM
Last modification on : Thursday, January 20, 2022 - 5:30:47 PM
Long-term archiving on: : Thursday, April 11, 2013 - 4:08:21 AM


Files produced by the author(s)


  • HAL Id : hal-00772599, version 1



Dale Miller. Reasoning about computations using two-levels of logic. APLAS 2010: Eighth Asian Symposium on Programming Languages and Systems, 2010, Shanghai, China. ⟨hal-00772599⟩



Record views


Files downloads