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, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
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.
Type de document :
Communication dans un congrès
APLAS 2010: Eighth Asian Symposium on Programming Languages and Systems, 2010, Shanghai, China. 2010
Liste complète des métadonnées

Littérature citée [45 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00772599
Contributeur : Dale Miller <>
Soumis le : jeudi 10 janvier 2013 - 17:56:41
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : jeudi 11 avril 2013 - 04:08:21

Fichier

aplas10.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00772599, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

216

Téléchargements de fichiers

76