×

Proof checking and logic programming. (English) Zbl 1362.68056


MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
68N17 Logic programming
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[1] Andreoli JM (1992) Logic programming with focusing proofs in linear logic. J Logic Comput 2(3): 297-347 · Zbl 0764.03020 · doi:10.1093/logcom/2.3.297
[2] Assaf A (2015) A framework for defining computational higher-order logics. PhD thesis, École Polytechnique · Zbl 0764.03020
[3] Baelde D (2012) Least and greatest fixed points in linear logic. ACM Trans Comput Logic 13(1) · Zbl 1352.03072
[4] Baelde D, Chaudhuri K, Gacek A, Miller D, Nadathur G, Tiu A, Wang Y (2014) Abella: a system for reasoning about relational specifications. J Formal Reas 7(2) · Zbl 1451.68315
[5] Baelde, D.; Gacek, A.; Miller, D.; Nadathur, G.; Tiu, A.; Pfenning, F. (ed.), The Bedwyr system for model checking over syntactic expressions, 391-397 (2007), New York
[6] Boyer RS, Moore JS (1979) A computational logic. Academic Press, New York · Zbl 0448.68020
[7] Baelde, D.; Miller, D.; Dershowitz, N. (ed.); Voronkov, A. (ed.), Least and greatest fixed points in linear logic, 92-106 (2007), New York · Zbl 1137.03323
[8] Blanco, R.; Miller, D.; Cervesato, I. (ed.); Schürmann, C. (ed.), Proof outlines as proof certificates: a system description, 7-14 (2015), Virginia
[9] Cousineau D, Dowek G (2007) Embedding pure type systems in the lambda-Pi-calculus modulo. In: Ronchi Della Rocca S (ed) Typed lambda calculi and applications, 8th international conference, TLCA 2007, Paris, France, June 26-28, 2007, proceedings, vol 4583. LNCS, Springer, Berlin, pp 102-117 · Zbl 1215.03021
[10] Church A (1940) A formulation of the simple theory of types. J Symbol Logic 5: 56-68 · JFM 66.1192.06 · doi:10.2307/2266170
[11] Chihani, Z.; Libal, T.; Reis, G.; De Nivelle, H. (ed.), The proof certifier Checkers, 201-210 (2015), Berlin · Zbl 1471.68305 · doi:10.1007/978-3-319-24312-2_14
[12] Chihaniz MD (2016) Proof certificates for equality reasoning. In: Benevides M, Thiemann R (ed) Post-proceedings of LSFA 2015: 10th workshop on logical and semantic frameworks, with applications. Natal, Brazil, vol 323. ENTCS, UK
[13] Chihani Z, Miller D, Renaud F (2013) Foundational proof certificates in first-order logic. In: Paola Bonacina M (ed) CADE 24: conference on automated deduction 2013, vol 7898. LNAI, Berlin, pp 162-177 · Zbl 1381.68261
[14] Chihani Z, Miller D, Renaud F (2016) A semantic framework for proof evidence. J Autom Reas (Published electronically). doi:10.1007/s10817-016-9380-6 · Zbl 1425.68371
[15] Chaudhuri K, Pfenning F, Price G (2008) A logical characterization of forward and backward chaining in the inverse method. J Autom Reas 40(2-3): 133-177 · Zbl 1151.03006 · doi:10.1007/s10817-007-9091-0
[16] The Dedukti system (2013). https://www.rocq.inria.fr/deducteam/Dedukti/index.html · Zbl 1290.68088
[17] Dunchev C, Guidi F, Coen CS, Tassi E (2015) ELPI: fast, embeddable, \[{\lambda}\] λProlog interpreter. In: Davis M, Fehnker A, McIver A, Voronkov A (eds) Logic for programming, artificial intelligence, and reasoning—20th international conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, proceedings, vol 9450. LNCS, Springer, Berlin, pp 460-468 · Zbl 1471.68046
[18] Danos, V.; Joinet, JB; Schellinx, H.; Girard, JY (ed.); Lafont, Y. (ed.); Regnier, L. (ed.), LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication, 211-224 (1995), Cambridge · Zbl 0829.03031
[19] Dyckhoff R, Lengrand S (2007) Call-by-value \[{\lambda}\] λ-calculus and LJQ. J Logic Comput 17(6): 1109-1134 · Zbl 1133.03030 · doi:10.1093/logcom/exm037
[20] Gentzen, G.; Szabo, ME (ed.), Investigations into logical deduction, 68-131 (1935), Amsterdam
[21] Girard JY (1987) Linear logic. Theor Comput Sci 50: 1-102 · Zbl 0625.03037 · doi:10.1016/0304-3975(87)90045-4
[22] Girard JY (1991) A new constructive logic: classical logic. Math Struct Comput Sci 1: 255-296 · Zbl 0752.03027 · doi:10.1017/S0960129500001328
[23] Girard JY (1992) A fixpoint theorem in linear logic. An email posting to the mailing list linear@cs.stanford.edu
[24] Gacek A, Miller D, Nadathur G (2012) A two-level logic approach to reasoning about computations. J Autom Reas 49(2): 241-273 · Zbl 1290.68088 · doi:10.1007/s10817-011-9218-1
[25] Gordon MJ, Milner AJ, Wadsworth CP (1979) Edinburgh LCF: a mechanised logic of computation, vol 78. LNCS, Springer, Berlin · Zbl 0421.68039 · doi:10.1007/3-540-09724-4
[26] Gonthier, G.; Kapur, D. (ed.), The four colour theorem: engineering of a formal proof, 333 (2007), Berlin · Zbl 1166.68346
[27] Hales TC (2005) A proof of the Kepler conjecture. Ann Math 162(3): 1065-1185 · Zbl 1096.52010 · doi:10.4007/annals.2005.162.1065
[28] Herbelin H (1995) S équents qu’on calcule: de l’interprétation du calcul des séquents comme calcul de lambda-termes et comme calcul de stratégies gagnantes. PhD thesis, Université Paris 7 · Zbl 1423.68475
[29] Harper R, Honsell F, Plotkin G (1993) A framework for defining logics. J ACM 40(1): 143-184 · Zbl 0778.03004 · doi:10.1145/138027.138060
[30] Heath, Q.; Miller, D.; Kaliszyk, C. (ed.); Paskevich, A. (ed.), A framework for proof certificates in finite state exploration, 11-26 (2015), Virginia
[31] Howe J.M (1998) Proof search issues in some non-classical logics. PhD thesis, University of St Andrews. University of St Andrews Research Report CS/99/1 · Zbl 1096.52010
[32] Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S (2009) seL4: formal verification of an OS kernel. In: Proceedings of the 22nd symposium on operating systems principles (22nd SOSP’09), operating systems review (OSR). ACM SIGOPS, Big Sky, pp 207-220
[33] Konev B, Lisitsa A (2014) A SAT attack on the Erdős discrepancy conjecture. In: International conference on theory and applications of satisfiability testing, vol 8561. LNCS, Springer, Berlin, pp 219-226 · Zbl 1343.68217
[34] Laurent O (2002) Etude de la polarisation en logique. PhD thesis, Université Aix-Marseille II
[35] Leroy X (2009) Formal verification of a realistic compiler. Commun. ACM 52(7): 107-115 · doi:10.1145/1538788.1538814
[36] Liang C, Miller D (2009) Focusing and polarization in linear, intuitionistic, and classical logics. Theor Comput Sci 410(46): 4747-4768 · Zbl 1187.68528 · doi:10.1016/j.tcs.2009.07.041
[37] Meng J (2015) The integration of higher order interactive proof with first order automatic theorem proving. PhD thesis, University of Cambridge, Computer Laboratory
[38] Milner R (1989) Communication and concurrency. Prentice-Hall International, USA · Zbl 0683.68008
[39] Miller, D.; Odifreddi, P. (ed.), Abstractions in logic programming, 329-359 (1990), New York
[40] Miller D (2011) ProofCert: broad spectrum proof certificates. An ERC advanced grant funded for the five years 2012-2016
[41] Miller, D.; Jouannaud, JP (ed.); Shao, Z. (ed.), A proposal for broad spectrum proof certificates, 54-69 (2011), Berlin · Zbl 1349.03027
[42] Miller D (2014) Communicating and trusting proofs: the case for broad spectrum proof certificates. In: Schroeder-Heister P, Hodges W, Heinzmann G, Bour PE (eds) Logic, methodology, and philosophy of science. Proceedings of the fourteenth international congress. College Publications, Wenham, pp 323-342 · Zbl 1366.03100
[43] McDowell R, Miller D (2000) Cut-elimination for a logic with definitions and induction. Theor Comput Sci 232: 91-119 · Zbl 0951.03050 · doi:10.1016/S0304-3975(99)00171-1
[44] Marin S, Miller D, Volpe M (2016) A focused framework for emulating modal proof systems. In: Advances in modal logics (To appear) · Zbl 1400.03048
[45] Miller D, Nadathur G (2012) Programming with higher-order logic. Cambridge University Press, Cambridge · Zbl 1267.68014 · doi:10.1017/CBO9781139021326
[46] Miller D, Nadathur G, Pfenning F, Scedrov A (1991) Uniform proofs as a foundation for logic programming. Ann Pure Appl Logic 51: 125-157 · Zbl 0721.03037 · doi:10.1016/0168-0072(91)90068-W
[47] Miller D, Tiu A (2005) A proof theory for generic judgments. ACM Trans Comput Logic 6(4): 749-783 · Zbl 1367.03059 · doi:10.1145/1094622.1094628
[48] Miller, D.; Volpe, M.; Davis, M. (ed.); Fehnker, A. (ed.); McIver, A. (ed.); Voronkov, A. (ed.), Focused labeled proof systems for modal logic, 266-280 (2015), Berlin · Zbl 1471.03048 · doi:10.1007/978-3-662-48899-7_19
[49] Nadathur G, Mitchell DJ (1999) System description: Teyjus—a compiler and abstract machine based implementation of \[{\lambda}\] λProlog. In: Ganzinger H (ed) 16th conf. on automated deduction (CADE), vol 1632. LNAI, Springer, Trento, pp 287-291
[50] Necula GC, Rahul SP (2001) Oracle-based checking of untrusted software. In: Hankin C, Schmidt D (eds) 28th ACM symp. on principles of programming languages, pp 142-154 · Zbl 1323.68222
[51] Pereira F (1988) C-Prolog user’s manual, version 1.5
[52] Pfenning F, Schürmann C (1999) System description: Twelf—a meta-logical framework for deductive systems. In: Ganzinger H (ed) 16th conf. on automated deduction (CADE), vol 1632. LNAI, Springer, Trento, pp 202-206
[53] Schroeder-Heister, P.; Vardi, M. (ed.), Rules of definitional reflection, 222-232 (1993), IEEE
[54] Tiu A, Nadathur G, Miller D (2005) Mixing finite success and finite failure in an automated prover. In: Empirically successful automated reasoning in higher-order logics (ESHOL’05), pp 79-98 · Zbl 1367.03059
[55] Wetzler, N.; Heule, MJH; Hunt, JWA; Sinz, C. (ed.); Egly, U. (ed.), DRAT-trim: efficient checking and trimming using expressive clausal proofs, 422-429 (2014), Berlin · Zbl 1423.68475
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.