Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Verification of Concurrent Programs on Weak Memory Models Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti

verfasst von : Raphaël Cauderlier, Catherine Dubois

Erschienen in: Theoretical Aspects of Computing – ICTAC 2016

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

The programming environment FoCaLiZe allows the user to specify, implement, and prove programs with the help of the theorem prover Zenon. In the actual version, those proofs are verified by Coq. In this paper we propose to extend the FoCaLiZe compiler by a backend to the Dedukti language in order to benefit from Zenon Modulo, an extension of Zenon for Deduction modulo. By doing so, FoCaLiZe can benefit from a technique for finding and verifying proofs more quickly. The paper focuses mainly on the process that overcomes the lack of local pattern-matching and recursive definitions in Dedukti.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Propositional Dynamic Logic for Petri Nets with Iteration
Nächstes Kapitel Parametric Deadlock-Freeness Checking Timed Automata
Fußnoten
2
The files can be obtained from http://​deducteam.​inria.​fr/​focalide.
 
Literatur
1.
Assaf, A.: A framework for defining computational higher-order logics. Ph.D. thesis, École Polytechnique (2015)
2.
Assaf, A., Burel, G.: Translating HOL to Dedukti. In: Kaliszyk, C., Paskevich, A. (eds.) Proceedings Fourth Workshop on Proof eXchange for Theorem Proving. EPTCS, vol. 186, Berlin, Germany, pp. 74–88 (2015)
3.
Bonichon, R., Delahaye, D., Doligez, D.: Zenon: an extensible automated theorem prover producing checkable proofs. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 151–165. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-75560-9_​13 CrossRef
4.
Burel, G.: A shallow embedding of resolution and superposition proofs into the \(\lambda {\varPi }\)-calculus modulo. In: Blanchette, J.C., Urban, J. (eds.) PxTP 2013. 3rd International Workshop on Proof Exchange for Theorem Proving. EasyChair Proceedings in Computing, vol. 14, Lake Placid, USA, pp. 43–57 (2013)
5.
Cauderlier, R.: Object-oriented mechanisms for interoperability between proof systems. Ph.D. thesis, Conservatoire National des Arts et Métiers, Paris (draft)
6.
Cauderlier, R., Dubois, C.: Objects and subtyping in the \(\lambda \varPi \)-calculus modulo. In: Post-proceedings of the 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl, Paris (2014)
7.
Cauderlier, R., Halmagrand, P.: Checking Zenon Modulo proofs in Dedukti. In: Kaliszyk, C., Paskevich, A. (eds.) Proceedings 4th Workshop on Proof eXchange for Theorem Proving. EPTCS, vol. 186, Berlin, Germany, pp. 57–73 (2015)
8.
Cousineau, D., Dowek, G.: Embedding pure type systems in the \(\lambda {\varPi }\)-calculus modulo. In: Rocca, S.R.D. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 102–117. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-73228-0_​9 CrossRef
9.
Delahaye, D., Doligez, D., Gilbert, F., Halmagrand, P., Hermant, O.: Zenon Modulo: when Achilles outruns the tortoise using deduction modulo. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19. LNCS, vol. 8312, pp. 274–290. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-45221-5_​20 CrossRef
10.
11.
Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for Haskell by term rewriting. ACM Trans. Program. Lang. Syst. 33(2), 7:1–7:39 (2011)CrossRef
12.
13.
Klop, J.W., van Oostrom, V., de Vrijer, R.: Lambda calculus with patterns. Theoret. Comput. Sci. 398(1–3), 16–31 (2008). Calculi, Types and Applications: Essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi Della RoccaMathSciNetCrossRefMATH
14.
Lucas, S., Peña, R.: Rewriting techniques for analysing termination and complexity bounds of Safe programs. In: LOPSTR 2008, pp. 43–57 (2008)
15.
Pessaux, F.: FoCaLiZe: inside an F-IDE. In: Dubois, C., Giannakopoulou, D., Méry, D. (eds.) Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014. EPTCS, vol. 149, Grenoble, France, pp. 64–78 (2014)
16.
Peyton Jones, S.L.: The Implementation of Functional Programming Languages. Prentice-Hall International Series in Computer Science. Prentice-Hall, Inc., Upper Saddle River (1987)MATH
17.
Saillard, R.: Type checking in the \(\lambda {\varPi }\)-calculus modulo: theory and practice. Ph.D. thesis, MINES Paritech (2015)
Metadaten
Titel
ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti
verfasst von
Raphaël Cauderlier
Catherine Dubois
Copyright-Jahr
2016
Buch
Theoretical Aspects of Computing – ICTAC 2016

Print ISBN: 978-3-319-46749-8

Electronic ISBN: 978-3-319-46750-4

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-46750-4_26

Premium Partner

    Bildnachweise