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:
Exploring an Interface Model for CKA Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

Auto in Agda

Programming Proof Search Using Reflection

verfasst von : Wen Kokke, Wouter Swierstra

Erschienen in: Mathematics of Program Construction

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

As proofs in type theory become increasingly complex, there is a growing need to provide better proof automation. This paper shows how to implement a Prolog-style resolution procedure in the dependently typed programming language Agda. Connecting this resolution procedure to Agda’s reflection mechanism provides a first-class proof search tactic for first-order Agda terms. As a result, writing proof automation tactics need not be different from writing any other program.

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 Turing-Completeness Totally Free
Nächstes Kapitel Fusion for Free
Fußnoten
2
Note that Agda’s reflection mechanism should not be confused with ‘proof by reflection’ – the technique of writing a verified decisionprocedure for some class of problems.
 
3
Syntax for Agda tactics was added in Agda 2.4.2.
 
Literatur
Allais, G.: Proof automatization using reflection (implementations in Agda). MSc Intern report, University of Nottingham (2010)
Chapman, J.: Type checking and normalisation. Ph.D. thesis, University of Nottingham (2009)
Chlipala, A.: Certified Programming with Dependent Types. MIT Press, Cambridge (2013)CrossRefMATH
Danielsson, N.A.: A formalisation of a dependently typed language as an inductive-recursive family. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 93–109. Springer, Heidelberg (2007). doi:10.​1145/​2500365.​2500575 CrossRef
Coq development team. The Coq proof assistant reference manual. Logical Project (2004)
Devriese, D., Piessens, F.: Typed syntactic meta-programming. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming (ICFP 2013). ACM, September 2013. doi:10.​1145/​2500365.​2500575
Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, New York (1993) MATH
Lindblad, F., Benke, M.: A tool for automated theorem proving in Agda. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 154–169. Springer, Heidelberg (2006) CrossRefMATH
Malecha, G., Chlipala, A., Braibant, T.: Compositional computational reflection. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 374–389. Springer, Heidelberg (2014) CrossRef
Martin-Löf, P.: Constructive mathematics and computer programming. In: Proceedings of a Discussion Meeting of the Royal Society of London on Mathematical Logic and Programming Languages, pp. 167–184. Prentice-Hall Inc. (1985)
McBride, C.: Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation. In: Proceedings of the 6th ACM SIGPLAN Workshop on Generic Programming, WGP 2010, pp. 1–12. ACM, New York (2010). doi:10.​1145/​1863495.​1863497
Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology (2007)
Norell, U.: Dependently typed programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230–266. Springer, Heidelberg (2009a) CrossRefMATH
Norell, U.: Playing with Agda. Invited talk at TPHOLS (2009b)
Oury, N., Swierstra, W.: The power of Pi. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP 2008, pp. 39–50 (2008). doi:10.​1145/​1411204.​1411213
Jones, S.P. (ed.): Haskell 98 Language and Libraries: the Revised report. Cambridge University Press, Cambridge (2003) MATH
Pitman, K.M.: Special forms in LISP. In: Proceedings of the 1980 ACM Conference on LISP and Functional Programming, pp. 179–187. ACM (1980)
Sheard, T., Jones, S.P.: Template meta-programming for Haskell. In: Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell, pp 1–16 (2002). doi:10.​1145/​581690.​581691
Stutterheim, J., Swierstra, W., Swierstra, D.: Forty hours of declarative programming: teaching prolog at the junior college Utrecht. In: Proceedings First International Workshop on Trends in Functional Programming in Education, Electronic Proceedings in Theoretical Computer Science, University of St. Andrews, Scotland, UK, 11 June 2012, vol. 106, pp 50–62 (2013)
Taha, W., Sheard, T.: Multi-stage programming with explicit annotations. In: Proceedings of the 1997 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM 1997 (1997). doi:10.​1145/​258993.​259019
van der Walt, P., Swierstra, W.: Engineering proof by reflection in Agda. In: Hinze, R. (ed.) IFL 2012. LNCS, vol. 8241, pp. 157–173. Springer, Heidelberg (2013) CrossRef
Ziliani, B., Dreyer, D., Krishnaswami, N.R., Nanevski, A., Vafeiadis, V.: Mtac: a monad for typed tactic programming in Coq. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, pp 87–100 (2013). doi:10.​1145/​2500365.​2500579
Metadaten
Titel
Auto in Agda
verfasst von
Wen Kokke
Wouter Swierstra
Copyright-Jahr
2015
Verlag
Springer International Publishing
Buch
Mathematics of Program Construction

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

Electronic ISBN: 978-3-319-19797-5

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-19797-5_14

Premium Partner

    Bildnachweise