25 Years of Formal Proof Cultures: Some Problems, Some Philosophy, Bright Future

Abstract : Throughout the history of Mathematics, several different proof cultures have co-existed, and still do co-exist. After 25 years of Logical Frameworks, we can say that even as far as proof metalanguages go, a definitive system is utopian and that we are witnessing the continuous development of a diversity of formal proof cultures, see e.g. [10–12, 17, 19, 21, 23, 24, 28]. In this paper, we propose a contribution towards the clarification of some controversial issues that have arisen in the theory and practice of Logical Frameworks, and have possibly motivated such a manifold speciation. Using as a running example the encoding of the critical features of Non-Commutative Linear Logic (NCLL) [26] in the Logical Framework LFP [20], we discuss the notions of adequacy of an encoding, locality of a side-condition, deep and shallow encodings, and how to embed heterogenous justifications or external evidence in LF. This discussion naturally leads to the question of how to express formally the expressive power of a Logical Framework, a minimal requirement being that of encoding itself within itself. We focus on LFP and we discuss its relations to the original LF [17], and briefly to the Conditional LF [21], and the Pattern LF [19] previously introduced by the authors. We conclude the paper by briefly comparing LFP to λΠ-calculus modulo [12], the Linear LF [9], and the Concurrent LF[28].
Type de document :
Communication dans un congrès
LFMTP 2013, Sep 2013, Boston, United States. ACM, pp.37-42, Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice - LFMTP 2013 - Boston, Massachusetts, USA. 〈10.1145/2503887.2503896〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01146393
Contributeur : Luigi Liquori <>
Soumis le : mercredi 13 mai 2015 - 10:37:29
Dernière modification le : mercredi 13 mai 2015 - 11:13:28
Document(s) archivé(s) le : mercredi 19 avril 2017 - 08:38:16

Fichier

2013-lfmtp-13.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Furio Honsell. 25 Years of Formal Proof Cultures: Some Problems, Some Philosophy, Bright Future. LFMTP 2013, Sep 2013, Boston, United States. ACM, pp.37-42, Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice - LFMTP 2013 - Boston, Massachusetts, USA. 〈10.1145/2503887.2503896〉. 〈hal-01146393〉

Partager

Métriques

Consultations de la notice

42

Téléchargements de fichiers

48