Reasoning about Computational Systems using Abella

Kaustuv Chaudhuri 1 Gopalan Nadathur 2
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
2 Departement of Electrical & Computer Engineering [Minneapolis]
Abstract : We present a tutorial on the Abella theorem prover that is designed to reason about relational specifications in higher-order abstract syntax.
Type de document :
Document associé à des manifestations scientifiques
Abella Tutorial, Aug 2015, Berlin, Germany. 2015
Liste complète des métadonnées
https://hal.inria.fr/hal-01222774
Contributeur : Kaustuv Chaudhuri <>
Soumis le : vendredi 30 octobre 2015 - 15:09:53
Dernière modification le : mercredi 14 novembre 2018 - 16:14:01
Document(s) archivé(s) le : vendredi 28 avril 2017 - 06:45:13

Fichier

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

Licence

Distributed under a Creative Commons Paternité - Pas de modifications 4.0 International License

Identifiants

  • HAL Id : hal-01222774, version 1

Collections

X | LIX | X-LIX | INRIA | INRIA-MECSCI | PARISTECH | UNIV-PARIS-SACLAY | X-DEP-INFO

Citation

Kaustuv Chaudhuri, Gopalan Nadathur. Reasoning about Computational Systems using Abella. Abella Tutorial, Aug 2015, Berlin, Germany. 2015. 〈hal-01222774〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

455

Téléchargements de fichiers

71

Contact


archive-ouverte@inria.fr