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
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
An Isabelle/HOL Formalisation of Green’s Theorem Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Equational Reasoning with Applicative Functors

verfasst von : Andreas Lochbihler, Joshua Schneider

Erschienen in: Interactive Theorem Proving

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

In reasoning about effectful computations, it often suffices to focus on the effect-free parts. We present a package for automatically lifting equations to effects modelled by applicative functors. It exploits properties of the concrete functor thanks to a modular classification based on combinators. We formalise the meta theory and demonstrate the usability of our Isabelle/HOL package with two case studies. This is a first step towards practical reasoning with effectful computations.

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 A Formal Proof of Cauchy’s Residue Theorem
Nächstes Kapitel Formally Verified Approximations of Definite Integrals
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
As lifting wraps the types of free variables in F, it does not look into abstractions, but treats them like constants. For example, https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-43144-4_16/419043_1_En_16_IEq60_HTML.gif is lifted to https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-43144-4_16/419043_1_En_16_IEq61_HTML.gif rather than https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-43144-4_16/419043_1_En_16_IEq62_HTML.gif . Thus, lifting effectively operates on first-order terms.
 
2
Hinze briefly considers functors with the combinators S and C and notes that the case with only the combinator C might be interesting, too, but omits the details.
 
3
The following shows the equivalence (bold face denotes doubling and underlining dropping of a repetition): https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-43144-4_16/419043_1_En_16_IEq234_HTML.gif .
 
Literatur
1.
Berghofer, S.: Proofs, Programs and Executable Specifications in Higher Order Logic. Ph.D. thesis, Institut für Informatik, Technische Universität München (2003)
2.
Berstel, J., Reutenauer, C.: Square-free words and idempotent semigroups. In: Lothaire, M. (ed.) Combinatorics on Words, 2nd edn., pp. 18–38. Cambridge University Press (1997)
3.
Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Abadi, M., Ito, T. (eds.) TACS 1997. LNCS, vol. 1281, pp. 515–529. Springer, Heidelberg (1997)
4.
Bulwahn, L., Krauss, A., Haftmann, F., Erkök, L., Matthews, J.: Imperative functional programming with Isabelle/HOL. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 134–149. Springer, Heidelberg (2008)CrossRef
5.
6.
Church, A.: The Calculi of Lambda-Conversion. Princeton University Press, Princeton (1941)MATH
7.
Dijkstra, E.W.: An exercise for Dr. R.M. Burstall. In: Selected Writings on Computing: A Personal Perspective. Texts and Monographs in Computer Science, pp. 215–216. Springer, New York (1982)
8.
Eberl, M., Hölzl, J., Nipkow, T.: A verified compiler for probability density functions. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 80–104. Springer, Heidelberg (2015)CrossRef
9.
10.
11.
Gibbons, J., Hinze, R.: Just do it: simple monadic equational reasoning. In: ICFP 2011, pp. 2–14. ACM (2011)
12.
Graham, R.L., Knuth, D.E., Patashnik, O.: Concrete Mathematics-A Foundation for Computer Science, 2nd edn. Addison-Wesley, Reading (1994)
13.
14.
15.
16.
Homeier, P.V.: The HOL-omega logic. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 244–259. Springer, Heidelberg (2009)CrossRef
17.
Huffman, B.: Transfer principle proof tactic for nonstandard analysis. In: Kanovich, M., White, G., Gottliebsen, H., Oliva, P. (eds.) NetCA 2005, pp. 18–26. Queen Mary, University of London, Dept. of Computer Science, Research report RR-05-06 (2005)
18.
Huffman, B., Kunčar, O.: Lifting and Transfer: a modular design for quotients in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131–146. Springer, Heidelberg (2013)CrossRef
19.
Hutton, G., Fulger, D.: Reasoning about effects: seeing the wood through the trees. In: Trends in Functional Programming (TFP 2008) (2008)
20.
Krebbers, R.: The C standard formalized in Coq. Ph.D. thesis, Radboud University (2015)
21.
Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft’s algorithm. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 166–182. Springer, Heidelberg (2012)CrossRef
22.
Lochbihler, A.: Probabilistic functions and cryptographic oracles in higher order logic. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 503–531. Springer, Heidelberg (2016)CrossRef
23.
24.
25.
McBride, C., Paterson, R.: Applicative programming with effects. J. Funct. Program. 18(1), 1–13 (2008)CrossRefMATH
26.
27.
28.
Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP 1983. Information Processing, vol. 83, pp. 513–523. North-Holland/IFIP (1983)
29.
Schropp, A., Popescu, A.: Nonfree datatypes in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 114–130. Springer, Heidelberg (2013)CrossRef
30.
Metadaten
Titel
Equational Reasoning with Applicative Functors
verfasst von
Andreas Lochbihler
Joshua Schneider
Copyright-Jahr
2016
Buch
Interactive Theorem Proving

Print ISBN: 978-3-319-43143-7

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

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-43144-4_16

Premium Partner

    Bildnachweise