nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

TWAM: A Certifying Abstract Machine for Logic Programs

verfasst von : Rose Bohrer, Karl Crary

Erschienen in: Verified Software. Theories, Tools, and Experiments

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

Type-preserving (or typed) compilation uses typing derivations to certify correctness properties of compilation. We have designed and implemented a typed compiler for an idealized logic programming language we call T-Prolog. The crux of our approach is a new certifying abstract machine which we call the Typed Warren Abstract Machine (TWAM). The TWAM has a dependent type system strong enough to show programs obey a semantics based on provability in first-order logic (FOL). We present a soundness metatheorem which (going beyond the guarantees provided by most typed compilers) constitutes a partial behavior correctness guarantee: well-typed TWAM programs are sound proof search procedures with respect to a FOL signature. We argue why this guarantee is a natural choice for significant classes of logic programs. This metatheorem justifies our design and implementation of a certifying compiler from T-Prolog to TWAM.

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 Program Verification in the Presence of I/O

Nächstes Kapitel A Java Bytecode Formalisation

See Sect. 6 for how these features might be supported.

Note that Query has no free variables. This simplifies the proof of Theorem 1 because it depends heavily on substitution reasoning.

Our running example is untyped (\(a=\mathtt{term}{}\) throughout) because untyped Prolog is well-known, but we will still present the typing rules in their full generality.

While this approach is preferable for the proofs, it is quite unreadable, so we used readable names in our presentation of the example instead.

Aït-Kaci, H.: Warren’s Abstract Machine: A Tutorial Reconstruction. MIT Press, Cambridge (1991)CrossRef

Aref, M., et al.: Design and implementation of the LogicBlox system. In: Sellis, T.K., Davidson, S.B., Ives, Z.G. (eds.) Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data, Melbourne, Victoria, Australia, 31 May - 4 June, 2015, pp. 1371–1382. ACM (2015). http://doi.acm.org/10.1145/2723372.2742796

Beierle, C., Börger, E.: Correctness proof for the WAM with types. In: Börger, E., Jäger, G., Kleine Büning, H., Richter, M.M. (eds.) CSL 1991. LNCS, vol. 626, pp. 15–34. Springer, Heidelberg (1992). https://doi.org/10.1007/BFb0023755CrossRef

Bohrer, R., Crary, K.: TWAM: a certifying abstract machine for logic programs. CoRR abs/1801.00471 (2018). http://arxiv.org/abs/1801.00471

Börger, E., Rosenzweig, D.: The WAM–definition and compiler correctness. In: Logic Programming: Formal Methods and Practical Applications, pp. 20–90 (1995)

Bowman, W.J., Ahmed, A.: Typed closure conversion for the calculus of constructions. In: Foster and Grossman [10], pp. 797–811. https://doi.org/10.1145/3192366.3192372

Crary, K.: Toward a foundational typed assembly language. In: Aiken, A., Morrisett, G. (eds.) Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New Orleans, Louisisana, USA, 15–17 January 2003, pp. 198–212. ACM (2003). https://doi.org/10.1145/640128.604149

Crary, K., Sarkar, S.: Foundational certified code in the Twelf metalogical framework. ACM Trans. Comput. Log. 9(3), 16:1–16:26 (2008). https://doi.org/10.1145/1352582.1352584

Crary, K., Vanderwaart, J.: An expressive, scalable type theory for certified code. In: Wand, M., Jones, S.L.P. (eds.) Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP 2002), Pittsburgh, Pennsylvania, USA, 4–6 October 2002, pp. 191–205. ACM (2002). https://doi.org/10.1145/581478.581497

10.

Foster, J.S., Grossman, D. (eds.): Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, 18–22 June 2018. ACM (2018). https://doi.org/10.1145/3192366

11.

Gacek, A.: System description: Abella - a system for reasoning about computations. CoRR 2008 (2008). http://arxiv.org/abs/0803.2305

12.

Hajiyev, E., et al.: Keynote address: QL for source code analysis. In: Seventh IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2007) (SCAM), pp. 3–16, October 2007. https://doi.org/10.1109/SCAM.2007.31

13.

Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. J. ACM 40(1), 143–184 (1993). https://doi.org/10.1145/138027.138060MathSciNetCrossRefMATH

14.

Kang, J., et al.: Crellvm: verified credible compilation for LLVM. In: Foster and Grossman [10], pp. 631–645. https://doi.org/10.1145/3192366.3192377

15.

Kriener, J., King, A., Blazy, S.: Proofs you can believe in: proving equivalences between prolog semantics in Coq. In: Peña, R., Schrijvers, T. (eds.) 15th International Symposium on Principles and Practice of Declarative Programming, PPDP 2013, Madrid, Spain, 16–18 September 2013, pp. 37–48. ACM (2013). https://doi.org/10.1145/2505879.2505886

16.

Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: POPL 2014, pp. 179–191 (2014). https://doi.org/10.1145/2535838.2535841

17.

Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Morrisett, J.G., Jones, S.L.P. (eds.) Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, 11–13 January 2006, pp. 42–54. ACM (2006). https://doi.org/10.1145/1111037.1111042

18.

Martelli, A., Montanari, U.: An efficient unification algorithm. ACM Trans. Program. Lang. Syst. 4(2), 258–282 (1982). https://doi.org/10.1145/357162.357169CrossRefMATH

19.

Morrisett, J.G., Crary, K., Glew, N., Walker, D.: Stack-based typed assembly language. J. Funct. Program. 13(5), 957–959 (2003). https://doi.org/10.1017/S0956796802004446CrossRefMATH

20.

Morrisett, J.G., Walker, D., Crary, K., Glew, N.: From system F to typed assembly language. ACM Trans. Program. Lang. Syst. 21(3), 527–568 (1999). https://doi.org/10.1145/319301.319345CrossRefMATH

21.

Myreen, M.O., Owens, S.: Proof-producing translation of higher-order logic into pure and stateful ML. J. Funct. Program. 24(2–3), 284–315 (2014). https://doi.org/10.1017/S0956796813000282MathSciNetCrossRefMATH

22.

Nadathur, G., Miller, D.: An overview of Lambda-PROLOG. In: Kowalski, R.A., Bowen, K.A. (eds.) Logic Programming, Proceedings of the Fifth International Conference and Symposium, Seattle, Washington, USA, 15–19 August 1988, vol. 2, pp. 810–827. MIT Press (1988)

23.

Necula, G.C., Lee, P.: The design and implementation of a certifying compiler. In: Davidson, J.W., Cooper, K.D., Berman, A.M. (eds.) Proceedings of the ACM SIGPLAN ’98 Conference on Programming Language Design and Implementation (PLDI), Montreal, Canada, 17–19 June 1998, pp. 333–344. ACM (1998). https://doi.org/10.1145/277650.277752

24.

Pfenning, F.: Elf: A language for logic definition and verified metaprogramming. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS 1989), Pacific Grove, California, USA, 5–8 June 1989, pp. 313–322. IEEE Computer Society (1989). https://doi.org/10.1109/LICS.1989.39186

25.

Pfenning, F.: Logic programming in the LF logical framework. In: Logical Frameworks, pp. 149–181. Cambridge University Press, New York (1991). http://dl.acm.org/citation.cfm?id=120477.120483

26.

Pfenning, F., Schürmann, C.: System description: Twelf—a meta-logical framework for deductive systems. In: CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48660-7_14CrossRef

27.

Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151–166. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0054170CrossRef

28.

Pusch, C.: Verification of compiler correctness for the WAM. In: Goos, G., Hartmanis, J., van Leeuwen, J., von Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 347–361. Springer, Heidelberg (1996). https://doi.org/10.1007/BFb0105415CrossRef

29.

Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965). https://doi.org/10.1145/321250.321253MathSciNetCrossRefMATH

30.

Russinoff, D.M.: A verified prolog compiler for the warren abstract machine. J. Log. Program. 13(4), 367–412 (1992). https://doi.org/10.1016/0743-1066(92)90054-7MathSciNetCrossRefMATH

31.

Schellhorn, G., Ahrendt, W.: Reasoning about abstract state machines: the WAM case study. J. UCS 3(4), 377–413 (1997). https://doi.org/10.3217/jucs-003-04-0377MathSciNetCrossRefMATH

32.

Sørensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism, vol. 149. Elsevier, Amsterdam (2006)MATH

33.

Spoto, F., Levi, G.: Abstract interpretation of prolog programs. In: Haeberer, A.M. (ed.) AMAST 1999. LNCS, vol. 1548, pp. 455–470. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-49253-4_32CrossRef

34.

Tarditi, D., Morrisett, J.G., Cheng, P., Stone, C.A., Harper, R., Lee, P.: TIL: a type-directed optimizing compiler for ML. In: PLDI, pp. 181–192. ACM (1996)

35.

Warren, D.H.: An Abstract Prolog Instruction Set, vol. 309. Artificial Intelligence Center, SRI International Menlo Park, California (1983)

36.

Wielemaker, J.: SWI-Prolog OpenHub Project Page (2018). https://www.openhub.net/p/swi-prolog. Accessed 28 Apr 2018

37.

Xi, H., Harper, R.: A dependently typed assembly language. In: Pierce, B.C. (ed.) Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP 2001), Florence, Italy, 3–5 September 2001, pp. 169–180. ACM (2001). https://doi.org/10.1145/507635.507657

38.

Xi, H., Pfenning, F.: Dependent types in practical programming. In: Appel, A.W., Aiken, A. (eds.) POPL 1999, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, 20–22 January 1999, pp. 214–227. ACM (1999). https://doi.org/10.1145/292540.292560

Titel: TWAM: A Certifying Abstract Machine for Logic Programs
verfasst von: Rose Bohrer
Karl Crary
Verlag: Springer International Publishing
Buch: Verified Software. Theories, Tools, and Experiments
Print ISBN: 978-3-030-03591-4

Electronic ISBN: 978-3-030-03592-1

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-030-03592-1_7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"