* Börger and Rosenzweig (1995b) Börger, E. and Rosenzweig, D. 1995b.  The WAM - definition and compiler correctness.  In Logic Programming: Formal Methods and Practical Applications, Studies in Computer Science and Artificial Intelligence, C. Beierle and L. Plümer, Eds. Elsevier Science B.V./North-Holland, 20–90.
  * Borras et al. (1988) Borras, P., Clément, D., Despeyroux, T., Incerpi, J., Kahn, G., Lang, B., and Pascual, V. 1988\.  Centaur: the system.  In Third Annual Symposium on Software Development Environments (SDE3). ACM, Boston, 14–24.
  * Bowen (1982) Bowen, K. A. 1982\.  Programming with full first-order logic.  In Machine Intelligence 10, Hayes, Michie, and Pao, Eds. Ellis Horwood and John Wiley, 421–440.
  * Brewka et al. (2011) Brewka, G., Eiter, T., and Truszczynski, M. 2011\.  Answer set programming at a glance.  Commun. ACM 54, 12, 92–103.
  * Brock-Nannestad et al. (2015) Brock-Nannestad, T., Guenot, N., and Gustafsson, D. 2015\.  Computation in focused intuitionistic logic.  In Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming (PPDP), M. Falaschi and E. Albert, Eds. ACM, 43–54.
  * De Bruijn (1972) De Bruijn, N. G. 1972\.  Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with an application to the Church-Rosser theorem.  Indagationes Mathematicae 34, 5, 381–392.
  * Bruscoli and Guglielmi (2006) Bruscoli, P. and Guglielmi, A. 2006\.  On structuring proof search for first order linear logic.  Theoretical Computer Science 360, 1-3, 42–76.
  * Bugliesi et al. (1994) Bugliesi, M., Lamma, E., and Mello, P. 1994\.  Modularity in logic programming.  J. of Logic Programming 19/20, 443–502.
  * Buss (1998) Buss, S. R. 1998\.  An Introduction to Proof Theory.  In Handbook of Proof Theory, S. R. Buss, Ed.  Elsevier Science Publishers, Amsterdam, 1–78.
  * Cellucci (1987) Cellucci, C. 1987\.  Using full first order logic as a programming language.  In Proceedings of the conference on ‘Logic and Computer Science: New Trends and Applications’. Rendiconti del Seminario Matematico Universitae Politecnico di Torino. Fascicolo Speciale 1987. 115–152.
  * Cervesato (1998) Cervesato, I. 1998\.  Proof-theoretic foundation of compilation in logic programming languages.  In Proceedings of the 1998 Joint International Conference and Symposium on Logic Programming, J. Jaffar, Ed. 115–129.
  * Cervesato et al. (2000) Cervesato, I., Hodas, J. S., and Pfenning, F. 2000\.  Efficient resource management for linear logic proof search.  Theoretical Computer Science 232, 1-2, 133–163.
  * Cervesato and Pfenning (1996) Cervesato, I. and Pfenning, F. 1996\.  A linear logic framework.  In 11th Symp. on Logic in Computer Science. IEEE Computer Society Press, New Brunswick, New Jersey, 264–275.
  * Chaudhuri (2006) Chaudhuri, K. 2006\.  The focused inverse method for linear logic.  Ph.D. thesis, Carnegie Mellon University.  Technical report CMU-CS-06-162.
  * Chaudhuri (2010a) Chaudhuri, K. 2010a.  Classical and intuitionistic subexponential logics are equally expressive.  In CSL 2010: Computer Science Logic, A. Dawar and H. Veith, Eds. LNCS, vol. 6247. Springer, Brno, Czech Republic, 185–199.
  * Chaudhuri (2010b) Chaudhuri, K. 2010b.  Magically constraining the inverse method using dynamic polarity assignment.  In Proc. 17th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), C. Fermüller and A. Voronkov, Eds. LNCS, vol. 6397. Springer, Yogyakarta, Indonesia, 202–216.
  * Chaudhuri et al. (2008) Chaudhuri, K., Pfenning, F., and Price, G. 2008\.  A logical characterization of forward and backward chaining in the inverse method.  J. of Automated Reasoning 40, 2-3 (Mar.), 133–177.
  * Chaudhuri and Reis (2015) Chaudhuri, K. and Reis, G. 2015\.  An adequate compositional encoding of bigraph structure in linear logic with subexponentials.  In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), M. Davis, A. Fehnker, A. McIver, and A. Voronkov, Eds. LNCS, vol. 9450. Springer, 146–161.
  * Chen et al. (1993) Chen, W., Kifer, M., and Warren, D. S. 1993\.  HILOG: a foundation for higher-order logic programming.  J. of Logic Programming 15, 3, 187–230.
  * Cheney and Urban (2004) Cheney, J. and Urban, C. 2004\.  Alpha-Prolog: A logic programming language with names, binding, and alpha-equivalence.  In Logic Programming, 20th International Conference, B. Demoen and V. Lifschitz, Eds. LNCS, vol. 3132. Springer, 269–283.
  * Chihani et al. (2017) Chihani, Z., Miller, D., and Renaud, F. 2017\.  A semantic framework for proof evidence.  J. of Automated Reasoning 59, 3, 287–330.
  * Church (1940) Church, A. 1940\.  A formulation of the Simple Theory of Types.  J. of Symbolic Logic 5, 56–68.
  * Clark (1978) Clark, K. L. 1978\.  Negation as failure.  In Logic and Data Bases, J. Gallaire and J. Minker, Eds. Plenum Press, New York, 293–322.
  * Clément et al. (1985) Clément, D., Despeyroux, J., Despeyroux, T., Hascoët, L., and Kahn, G. 1985\.  Natural semantics on the computer.  Research Report 416, INRIA, Rocquencourt, France. June.
  * Clocksin and Mellish (1994) Clocksin, W. F. and Mellish, C. S. 1994\.  Programming in Prolog, Fourth ed.  Springer.
  * Colmerauer and Roussel (1993) Colmerauer, A. and Roussel, P. 1993\.  The birth of Prolog.  SIGPLAN Notices 28, 3 (Mar.), 37–52.
  * Curien and Munch-Maccagnoni (2010) Curien, P. and Munch-Maccagnoni, G. 2010\.  The duality of computation under focus.  In Theoretical Computer Science - 6th IFIP TC 1/WG 2.2 International Conference, C. S. Calude and V. Sassone, Eds. IFIP Advances in Information and Communication Technology, vol. 323. Springer, 165–181.
  * Curry (1934) Curry, H. B. 1934\.  Functionality in combinatory logic.  Proceedings of the National Academy of Sciences 20, 11, 584–590.
  * Danos et al. (1993) Danos, V., Joinet, J.-B., and Schellinx, H. 1993\.  The structure of exponentials: Uncovering the dynamics of linear logic proofs.  In Kurt Gödel Colloquium, G. Gottlob, A. Leitsch, and D. Mundici, Eds. LNCS, vol. 713. Springer, 159–171.
  * Danos et al. (1995) Danos, V., Joinet, J.-B., and Schellinx, H. 1995\.  LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication.  In Advances in Linear Logic, J.-Y. Girard, Y. Lafont, and L. Regnier, Eds. Number 222 in London Mathematical Society Lecture Note Series. Cambridge University Press, 211–224.
  * Despeyroux (1986) Despeyroux, J. 1986\.  Proof of translation in natural semantics.  In 1st Symp. on Logic in Computer Science (LICS). IEEE, Cambridge, Mass, 193–205.
  * Despeyroux et al. (1995) Despeyroux, J., Felty, A., and Hirschowitz, A. 1995\.  Higher-order abstract syntax in Coq.  In Second International Conference on Typed Lambda Calculi and Applications. Springer, 124–138.
  * Despeyroux et al. (2016) Despeyroux, J., Olarte, C., and Pimentel, E. 2016\.  Hybrid and subexponential linear logics technical report.  In Proceedings of LSFA. ENTCS, vol. 332. Elsevier.
  * Despeyroux (1984) Despeyroux, T. 1984\.  Executable specification of static semantics.  In Semantics of Data Types. LNCS, vol. 173. Springer.
  * Despeyroux (1988) Despeyroux, T. 1988\.  TYPOL: A formalism to implement natural semantics.  Research Report 94, INRIA, Rocquencourt, France. Mar.
  * Di Cosmo and Miller (2019) Di Cosmo, R. and Miller, D. 2019\.  Linear Logic.  The Stanford Encyclopedia of Philosophy (Summer 2019 Edition), Edward N. Zalta (ed.).  https://plato.stanford.edu/archives/sum2019/entries/logic-linear/.
  * Donzeau-Gouge et al. (1984) Donzeau-Gouge, V., Huet, G., and Kahn, G. 1984\.  Programming environments based on structured editors: the MENTOR experience.  In Interactive Programming Environments, D. R. Barstow, H. E. Shrobe, and E. Sandewall, Eds. McGraw-Hill.
  * Dowling and Gallier (1984) Dowling, W. F. and Gallier, J. H. 1984\.  Linear-time algorithms for testing the satisfiability of propositional Horn formulae.  J. of Logic Programming 3, 267–284.
  * Dunchev et al. (2015) Dunchev, C., Guidi, F., Coen, C. S., and Tassi, E. 2015\.  ELPI: fast, embeddable, $\lambda$Prolog interpreter.  In Logic for Programming, Artificial Intelligence, and Reasoning \- 20th International Conference, LPAR-20, M. Davis, A. Fehnker, A. McIver, and A. Voronkov, Eds. LNCS, vol. 9450. Springer, 460–468.
  * Dyckhoff and Lengrand (2006) Dyckhoff, R. and Lengrand, S. 2006\.  LJQ: a strongly focused calculus for intuitionistic logic.  In Computability in Europe 2006, A. Beckmann and _et al._ , Eds. LNCS, vol. 3988. Springer, 173–185.
  * Earley (1970) Earley, J. 1970\.  An efficient context-free parsing algorithm.  Communications of the ACM 13, 2, 94–102.
  * Elliott (1989) Elliott, C. 1989\.  Higher-order unification with dependent types.  In Rewriting Techniques and Applications. LNCS, vol. 355. Springer, 121–136.
  * van Emden and Kowalski (1976) van Emden, M. H. and Kowalski, R. A. 1976\.  The semantics of predicate logic as a programming language.  J. of the ACM 23, 4, 733–742.
  * Espírito Santo (2016) Espírito Santo, J. E. 2016\.  The polarized $\lambda$-calculus.  In 11th Workshop on Logical and Semantic Frameworks with Applications, LSFA 2016, V. Nigam and M. Florido, Eds. Electronic Notes in Theoretical Computer Science, vol. 332. Elsevier, 149–168.
  * Fages et al. (1998) Fages, F., Ruet, P., and Soliman, S. 1998\.  Phase semantics and verification of concurrent constraint programs.  In 13th Symp. on Logic in Computer Science, V. Pratt, Ed. IEEE.
  * Fages et al. (2001) Fages, F., Ruet, P., and Soliman, S. 2001\.  Linear concurrent constraint programming: Operational and phase semantics.  Information and Computation 165, 1, 14–41.
  * Felty (1989) Felty, A. 1989\.  Specifying and implementing theorem provers in a higher-order logic programming language.  Ph.D. thesis, University of Pennsylvania.
  * Felty (1993) Felty, A. 1993\.  Implementing tactics and tacticals in a higher-order logic programming language.  J. of Automated Reasoning 11, 1, 43–81.
  * Felty and Miller (1990) Felty, A. and Miller, A. 1990\.  Encoding a Dependent-Type $\lambda$-Calculus in a Logic Programming Language.  In 10th Conf. on Automated Deduction (CADE), M. E. Stickel, Ed. LNAI, vol. 449. Springer, 221–235.
  * Friedman et al. (2018) Friedman, D. P., Byrd, W. E., Kiselyov, O., and Hemann, J. 2018\.  The Reasoned Schemer, Second Edition.  The MIT Press.
  * Gabbay (1985) Gabbay, D. M. 1985\.  N-Prolog: An extension of Prolog with hypothetical implication II—logical foundations, and negation as failure.  J. of Logic Programming 2, 4, 251–283.
  * Gabbay and Reyle (1984) Gabbay, D. M. and Reyle, U. 1984\.  N-Prolog: An extension of Prolog with hypothetical implications. I.  J. of Logic Programming 1, 319–355.
  * Gacek et al. (2011) Gacek, A., Miller, D., and Nadathur, G. 2011\.  Nominal abstraction.  Information and Computation 209, 1, 48–73.
  * Gacek et al. (2012) Gacek, A., Miller, D., and Nadathur, G. 2012\.  A two-level logic approach to reasoning about computations.  J. of Automated Reasoning 49, 2, 241–273.
  * Gallier (1986) Gallier, J. H. 1986\.  Logic for Computer Science: Foundations of Automatic Theorem Proving.  Harper $\&$ Row, 1986.
  * Ganzinger and McAllester (2002) Ganzinger, H. and McAllester, D. 2002\.  Logical algorithms.  In Proc. International Conference on Logic Programming (ICLP) 2002. LNCS, vol. 2401. Springer, 209–223.
  * Ganzinger and McAllester (2001) Ganzinger, H. and McAllester, D. A. 2001\.  A new meta-complexity theorem for bottom-up logic programs.  In First International Joint Conference on Automated Reasoning (IJCAR), R. Goré, A. Leitsch, and T. Nipkow, Eds. LNCS, vol. 2083. Springer, 514–528.
  * Gelfond and Lifschitz (1988) Gelfond, M. and Lifschitz, V. 1988\.  The stable model semantics for logic programming.  In Proceedings of the Fifth International Conference on Logic Programming, R. A. Kowalski and K. Bowen, Eds. The MIT Press, Cambridge, Massachusetts, 1070–1080.
  * Gentzen (1935) Gentzen, G. 1935\.  Investigations into logical deduction.  In The Collected Papers of Gerhard Gentzen, M. E. Szabo, Ed. North-Holland, Amsterdam, 68–131.  Translation of articles that appeared in 1934-35. Collected papers appeared in 1969.
  * Girard (1971) Girard, J.-Y. 1971\.  Une extension de l’interpretation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types.  In 2nd Scandinavian Logic Symposium, J. E. Fenstad, Ed. North-Holland, Amsterdam, 63–92.
  * Girard (1987) Girard, J.-Y. 1987\.  Linear logic.  Theoretical Computer Science 50, 1, 1–102.
  * Girard et al. (1989) Girard, J.-Y., Taylor, P., and Lafont, Y. 1989\.  _Proofs and Types_.  Cambridge University Press, 1989.
  * Girard (1991) Girard, J.-Y. 1991\.  A new constructive logic: classical logic.  Math. Structures in Comp. Science 1, 255–296.
  * Girard (1992) Girard, J.-Y. 1992\.  A fixpoint theorem in linear logic.  An email posting to the mailing list<EMAIL_ADDRESS>
  * Gödel (1930) Gödel, K. 1930\.  Die vollständigkeit der axiome des logischen funktionenkalküls.  Monatshefte für Mathematik 37, 1, 349–360.
  * Gordon (2000) Gordon, M. 2000\.  From LCF to HOL: a short history.  In Proof, Language, and Interaction: Essays in Honour of Robin Milner, G. D. Plotkin, C. Stirling, and M. Tofte, Eds. MIT Press, 169–186.
  * Gordon et al. (1979) Gordon, M. J., Milner, A. J., and Wadsworth, C. P. 1979\.  Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol. 78.  Springer.
  * Guglielmi (2007) Guglielmi, A. 2007\.  A system of interaction and structure.  ACM Trans. on Computational Logic 8, 1 (Jan.), 1–64.
  * Guidi et al. (2019) Guidi, F., Coen, C. S., and Tassi, E. 2019\.  Implementing type theory in higher order constraint logic programming.  Mathematical Structures in Computer Science 29, 8, 1125–1150.
  * Gunter and Gehlot (1989) Gunter, C. A. and Gehlot, V. 1989\.  Nets as tensor theories.  Tech. Rep. MS-CIS-89-68, University of Pennsylvania, Computer and Information Science Department. Oct.
  * Hagiya and Sakurai (1984) Hagiya, M. and Sakurai, T. 1984\.  Foundation of logic programming based on inductive definition.  New Generation Computing 2, 1, 59–77.
  * Hallnäs and Schroeder-Heister (1990) Hallnäs, L. and Schroeder-Heister, P. 1990\.  A proof-theoretic approach to logic programming. I. Clauses as rules.  J. of Logic and Computation 1, 2, 261–283.
  * Hallnäs and Schroeder-Heister (1991) Hallnäs, L. and Schroeder-Heister, P. 1991\.  A proof-theoretic approach to logic programming. II. Programs as definitions.  J. of Logic and Computation 1, 5, 635–660.
  * Hannan (1993) Hannan, J. 1993\.  Extended natural semantics.  J. of Functional Programming 3, 2, 123–152.
  * Hannan and Miller (1992) Hannan, J. and Miller, D. 1992\.  From operational semantics to abstract machines.  Mathematical Structures in Computer Science 2, 4, 415–459.
  * Hannan and Pfenning (1992) Hannan, J. and Pfenning, F. 1992\.  Compiler verification in LF.  In 7th Symp. on Logic in Computer Science. IEEE Computer Society Press, Santa Cruz, California.
  * Hannan (1990) Hannan, J. J. 1990\.  Investigating a proof-theoretic meta-language for functional programs.  Ph.D. thesis, University of Pennsylvania.
  * Haridi and Sahlin (1983) Haridi, S. and Sahlin, D. 1983\.  Evaluation of logic programs based on natural deduction (draft).  In Logic Programming Workshop, L. M. Pereira, A. Porto, L. Monteiro, and M. Figueiras, Eds. Núcleo de Intelligência Artificial, Universidade Nova De Lisboa, Portugal, 560–574.
  * Harland (1997) Harland, J. 1997\.  On goal-directed provability in classical logic.  Comput. Lang 23, 2-4, 161–178.
  * Harland et al. (1996) Harland, J., Pym, D., and Winikoff, M. 1996\.  Programming in Lygon: An overview.  In Proceedings of the Fifth International Conference on Algebraic Methodology and Software Technology, Eds. M. Wirsing and M. Nivat. LNCS, vol. 1101. Springer, 391–405.
  * Harper et al. (1993) Harper, R., Honsell, F., and Plotkin, G. 1993\.  A framework for defining logics.  J. of the ACM 40, 1, 143–184.
  * Harrop (1960) Harrop, R. 1960\.  Concerning formulas of the types $A\rightarrow B\lor C,\ A\rightarrow(Ex)B(x)$ in intuitionistic formal systems.  J. of Symbolic Logic 25, 27–32.
  * Heath and Miller (2019) Heath, Q. and Miller, D. 2019\.  A proof theory for model checking.  J. of Automated Reasoning 63, 4, 857–885.
  * Henkin (1949) Henkin, L. 1949\.  The completeness of the first-order functional calculus.  J. of Symbolic Logic 14, 3, 159–166.
  * Herbelin (1995) 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.  Ph.D. thesis, Université Paris 7.
  * Hodas and Miller (1991) Hodas, J. and Miller, D. 1991\.  Logic programming in a fragment of intuitionistic linear logic: Extended abstract.  In 6th Symp. on Logic in Computer Science, G. Kahn, Ed. IEEE, Amsterdam, 32–42.
  * Hodas and Miller (1994) Hodas, J. and Miller, D. 1994\.  Logic programming in a fragment of intuitionistic linear logic.  Information and Computation 110, 2, 327–365.
  * Hodas (1994) Hodas, J. S. 1994\.  Logic programming in intuitionistic linear logic: Theory, design, and implementation.  Ph.D. thesis, University of Pennsylvania, Department of Computer and Information Science.
  * Hodas and Tamura (2001) Hodas, J. S. and Tamura, N. 2001\.  lolliCop — A linear logic implementation of a lean connection-method theorem prover for first-order classical logic.  In Proceedings of IJCAR: International Joint Conference on Automated Reasoning, R. Goré, A. Leitsch, and T. Nipkow, Eds. LNCS, vol. 2083. Springer, 670–684.
  * Hofmann (1999) Hofmann, M. 1999\.  Semantical analysis of higher-order abstract syntax.  In 14th Symp. on Logic in Computer Science. IEEE Computer Society Press, 204–213.
  * Howard (1980) Howard, W. A. 1980\.  The formulae-as-type notion of construction, 1969.  In To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, J. P. Seldin and R. Hindley, Eds. Academic Press, New York, 479–490.
  * Howe (1998) Howe, J. M. 1998\.  Proof Search Issues in Some Non-Classical Logics.  Ph.D. thesis, University of St Andrews.  Available as University of St Andrews Research Report CS/99/1.
  * Huet and Lang (1978) Huet, G. and Lang, B. 1978\.  Proving and applying program transformations expressed with second-order patterns.  Acta Informatica 11, 31–55.
  * Huet (1973) Huet, G. P. 1973\.  A mechanization of type theory.  In Proceedings of the 3rd International Joint Conference on Artificial Intelligence. William Kaufmann, 139–146.
  * Huet (1975) Huet, G. P. 1975\.  A unification algorithm for typed $\lambda$-calculus.  Theoretical Computer Science 1, 27–57.
  * ISO.org (2000) ISO.org. 2000.  ISO/IEC 13211-2:2000: Information technology — programming languages — Prolog — part 2: Modules.
  * Jaffar and Lassez (1987) Jaffar, J. and Lassez, J.-L. 1987\.  Constraint logic programming.  In Proceedings of the 14th ACM Symposium on the Principles of Programming Languages. ACM.
  * Jagadeesan et al. (2005) Jagadeesan, R., Nadathur, G., and Saraswat, V. 2005\.  Testing concurrent systems: An interpretation of intuitionistic logic.  In FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science. LNCS, vol. 3821. Springer, Hyderabad, India, 517–528.
  * Kahn (1987) Kahn, G. 1987\.  Natural semantics.  In Proceedings of the Symposium on Theoretical Aspects of Computer Science, F.-J. Brandenburg, G. Vidal-Naquet, and M. Wirsing, Eds. LNCS, vol. 247. Springer, 22–39.
  * Kanovich et al. (2019) Kanovich, M., Kuznetsov, S., Nigam, V., and Scedrov, A. 2019\.  Subexponentials in non-commutative linear logic.  Mathematical Structures in Computer Science 29, 8, 1217–1249.
  * Kanovich (1995) Kanovich, M. I. 1995\.  Petri nets, Horn programs, Linear Logic and vector games.  Annals of Pure and Applied Logic 75, 1–2, 107–135.
  * Kobayashi and Yonezawa (1993) Kobayashi, N. and Yonezawa, A. 1993\.  ACL - A concurrent linear logic programming paradigm.  In Proceedings of the 1993 International Symposium on Logic Programming, D. Miller, Ed. MIT Press, 279–294.
  * Kobayashi and Yonezawa (1994) Kobayashi, N. and Yonezawa, A. 1994\.  Asynchronous communication model based on linear logic.  Formal Aspects of Computing 3, 279–294.
  * Kowalski (1979) Kowalski, R. A. 1979\.  Algorithm = Logic + Control.  Communications of the Association for Computing Machinery 22, 424–436.
  * Kowalski (1974) Kowalski, R. 1974\.  Predicate logic as a programming language.  Information Processing 74, 569–574.
  * Lambek (1958) Lambek, J. 1958\.  The mathematics of sentence structure.  American Mathematical Monthly 65, 154–169.
  * Li (1994) Li, B. Z. 1994\.  A $\pi$-calculus specification of Prolog.  In Proc. of European Symposium on Programming (ESOP 1994). LNCS, vol. 788. Springer, 379–393.
  * Liang and Miller (2007) Liang, C. and Miller, D. 2007\.  Focusing and polarization in intuitionistic logic.  In CSL 2007: Computer Science Logic, J. Duparc and T. A. Henzinger, Eds. LNCS, vol. 4646. Springer, 451–465.
  * Liang and Miller (2009) Liang, C. and Miller, D. 2009\.  Focusing and polarization in linear, intuitionistic, and classical logics.  Theoretical Computer Science 410, 46, 4747–4768.
  * Lifschitz (1996) Lifschitz, V. 1996\.  Foundations of logic programming.  In Principles of Knowledge Representation, G. Brewka, Ed. CSLI Publications, Stanford, California, 69–127.
  * Lifschitz (2008) Lifschitz, V. 2008\.  What is answer set programming?  In Proceedings of the 23rd National Conference on Artificial Intelligence. Vol. 3. AAAI Press, 1594–1597.
  * Lincoln (1995) Lincoln, P. 1995\.  Deciding provability of linear logic formulas.  In Proceedings of the workshop on Advances in linear logic, J.-Y. Girard, Y. Lafont, and L. Regnier, Eds. Cambridge University Press, New York, NY, USA, 197–210.
  * Lincoln and Saraswat (1993) Lincoln, P. and Saraswat, V. 1993\.  Higher-order, linear, concurrent constraint programming.  ftp://parcftp.xerox.com/pub/ccp/lcc/hlcc.dvi.
  * Lipton and Nieva (2018) Lipton, J. and Nieva, S. 2018\.  Kripke semantics for higher-order type theory applied to constraint logic programming languages.  Theoretical Computer Science 712, 1–37.
  * Lisitsa (2003) Lisitsa, A. 2003\.  $\lambda$leanTAP: Lean deduction in $\lambda$Prolog.  Tech. Rep. ULCS-03-017, University of Liverpool, Department of Computer Science.
  * Lloyd and Topor (1984) Lloyd, J. and Topor, R. 1984\.  Making Prolog more expressive.  J. of Logic Programming 1, 3 (Oct.), 225–240.
  * Lloyd and Shepherdson (1991) Lloyd, J. W. and Shepherdson, J. C. 1991\.  Partial evaluation in logic programming.  The J. of Logic Programming 11, 3, 217–242.
  * Loveland (1970) Loveland, D. W. 1970\.  A linear format for resolution.  In Symposium on Automatic Demonstration. Number 125 in Lecture Notes in Mathematics. Springer Verlag, Berlin, 147–162.
  * Loveland (1987) Loveland, D. W. 1987\.  Near-Horn PROLOG.  In Proceedings of the Fourth International Conference on Logic Programming, J.-L. Lassez, Ed. MIT Press Series in Logic Programming. The MIT Press, Melbourne, 456–469.
  * Loveland and Reed (1991) Loveland, D. W. and Reed, D. W. 1991\.  A near-Horn Prolog for compilation.  In Computational Logic - Essays in Honor of Alan Robinson, J.-L. Lassez and G. Plotkin, Eds. MIT Press, 542–564.
  * Luckham (1970) Luckham, D. 1970\.  Refinement theorems in resolution theory.  In Symposium on Automatic Demonstration. Number 125 in Lecture Notes in Mathematics. Springer Verlag, Berlin, 163–190.
  * Maier and Warren (1988) Maier, D. and Warren, D. S. 1988\.  Computing with Logic: Logic Programming with Prolog.  Addison-Wesley, Reading, MA.
  * Marek and Truszczyński (1993) Marek, W. and Truszczyński, M. 1993\.  Nonmonotonic logics: context-dependent reasoning.  Berlin: Springer-Verlag.
  * Martin-Löf (1971) Martin-Löf, P. 1971\.  Hauptsatz for the intuitionistic theory of iterated inductive definitions.  In Proceedings of the Second Scandinavian Logic Symposium, J. E. Fenstad, Ed. Studies in Logic and the Foundations of Mathematics, vol. 63. North-Holland, 179–216.
  * Martin-Löf (1982) Martin-Löf, P. 1982\.  Constructive mathematics and computer programming.  In Sixth International Congress for Logic, Methodology, and Philosophy of Science. North-Holland, Amsterdam, 153–175.
  * McCarty (1988a) McCarty, L. T. 1988a.  Clausal intuitionistic logic I. Fixed point semantics.  J. of Logic Programming 5, 1–31.
  * McCarty (1988b) McCarty, L. T. 1988b.  Clausal intuitionistic logic II. Tableau proof procedure.  J. of Logic Programming 5, 93–132.
  * McDowell and Miller (2000) McDowell, R. and Miller, D. 2000\.  Cut-elimination for a logic with definitions and induction.  Theoretical Computer Science 232, 91–119.
  * Michaylov and Pfenning (1992) Michaylov, S. and Pfenning, F. 1992\.  Natural semantics and some of its meta-theory in Elf.  In Extensions of Logic Programming, L.-H. Eriksson, L. Hallnäs, and P. Schroeder-Heister, Eds. LNCS, vol. 596. Springer, 299–344.
  * Miller (1989) Miller, D. 1989\.  A logical analysis of modules in logic programming.  J. of Logic Programming 6, 1-2, 79–108.
  * Miller (1991a) Miller, D. 1991a.  A logic programming language with lambda-abstraction, function variables, and simple unification.  J. of Logic and Computation 1, 4, 497–536.
  * Miller (1991b) Miller, D. 1991b.  Proof theory as an alternative to model theory.  Newsletter of the Association for Logic Programming 4, 3 (Aug.).  Guest editorial.
  * Miller (1992) Miller, D. 1992\.  Unification under a mixed prefix.  J. of Symbolic Computation 14, 4, 321–358.
  * Miller (1993) Miller, D. 1993\.  The $\pi$-calculus as a theory in linear logic: Preliminary results.  In 3rd Workshop on Extensions to Logic Programming, E. Lamma and P. Mello, Eds. LNCS, vol. 660. Springer, Bologna, Italy, 242–265.
  * Miller (1994) Miller, D. 1994\.  A multiple-conclusion meta-logic.  In 9th Symp. on Logic in Computer Science, S. Abramsky, Ed. IEEE Computer Society, Paris, 272–281.
  * Miller (1996) Miller, D. 1996\.  Forum: A multiple-conclusion specification logic.  Theoretical Computer Science 165, 1, 201–232.
  * Miller (2003) Miller, D. 2003\.  Encryption as an abstract data-type: An extended abstract.  In Proceedings of FCS’03: Foundations of Computer Security, I. Cervesato, Ed. ENTCS, vol. 84. Elsevier, 18–29.
  * Miller (2004) Miller, D. 2004\.  Overview of linear logic programming.  In Linear Logic in Computer Science, T. Ehrhard, J.-Y. Girard, P. Ruet, and P. Scott, Eds. London Mathematical Society Lecture Note, vol. 316. Cambridge University Press, 119–150.
  * Miller (2006) Miller, D. 2006\.  Representing and reasoning with operational semantics.  In Proceedings of IJCAR: International Joint Conference on Automated Reasoning, U. Furbach and N. Shankar, Eds. LNAI, vol. 4130. Springer, 4–20.
  * Miller (2008) Miller, D. 2008\.  A proof-theoretic approach to the static analysis of logic programs.  In Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday. Number 17 in Studies in Logic. College Publications, 423–442.
  * Miller (2017) Miller, D. 2017\.  Proof checking and logic programming.  Formal Aspects of Computing 29, 3, 383–399.
  * Miller (2019) Miller, D. 2019\.  Mechanized metatheory revisited.  J. of Automated Reasoning 63, 3, 625–665.
  * Miller (2021) Miller, D. 2021\.  Reciprocal influences between logic programming and proof theory.  Philosophy & Technology 34, 1 (Mar.), 75–104.
  * Miller and Nadathur (1986a) Miller, D. and Nadathur, G. 1986a.  Higher-order logic programming.  In Proceedings of the Third International Logic Programming Conference, E. Shapiro, Ed. LNCS, vol. 225. Springer, London, 448–462.
  * Miller and Nadathur (1986b) Miller, D. and Nadathur, G. 1986b.  Some uses of higher-order logic in computational linguistics.  In Proceedings of the 24th Annual Meeting of the Association for Computational Linguistics. Association for Computational Linguistics, Morristown, New Jersey, 247–255.
  * Miller and Nadathur (2012) Miller, D. and Nadathur, G. 2012\.  Programming with Higher-Order Logic.  Cambridge University Press.
  * Miller et al. (1991) Miller, D., Nadathur, G., Pfenning, F., and Scedrov, A. 1991\.  Uniform proofs as a foundation for logic programming.  Annals of Pure and Applied Logic 51, 1–2, 125–157.
  * Miller and Tiu (2005) Miller, D. and Tiu, A. 2005\.  A proof theory for generic judgments.  ACM Trans. on Computational Logic 6, 4 (Oct.), 749–783.
  * Milner (1979) Milner, R. 1979\.  LCF: A way of doing proofs with a machine.  In International Symposium on Mathematical Foundations of Computer Science. Springer, 146–159.
  * Milner et al. (1990) Milner, R., Tofte, M., and Harper, R. 1990\.  The Definition of Standard ML.  MIT Press.
  * Minker and Rajasekar (1990) Minker, J. and Rajasekar, A. 1990\.  A fixpoint semantics for disjunctive logic programs.  J. of Logic Programming 9, 1, 45–74.
  * Mints and Tyugu (1990) Mints, G. and Tyugu, E. 1990\.  Propositional logic programming and Priz system.  J. Logic Programming 9, 2&3, 179–193.
  * Mitchell and Moggi (1991) Mitchell, J. C. and Moggi, E. 1991\.  Kripke-style models for typed lambda calculus.  Annals of Pure and Applied Logic 51, 1-2, 99–124.
  * Nadathur (1987) Nadathur, G. 1987\.  A higher-order logic as the basis for logic programming.  Ph.D. thesis, University of Pennsylvania.
  * Nadathur (1993) Nadathur, G. 1993\.  A proof procedure for the logic of hereditary Harrop formulas.  J. of Automated Reasoning 11, 1, 115–145.
  * Nadathur (1998) Nadathur, G. 1998\.  Uniform provability in classical logic.  J. of Logic and Computation 8, 2, 209–229.
  * Nadathur (2000) Nadathur, G. 2000\.  Correspondences between classical, intuitionistic and uniform provability.  Theoretical Computer Science 232, 273–298.
  * Nadathur (2005) Nadathur, G. 2005\.  A treatment of higher-order features in logic programming.  Theory and Practice of Logic Programming 5, 3, 305–354.
  * Nadathur and Loveland (1995) Nadathur, G. and Loveland, D. 1995\.  Uniform proofs and disjunctive logic programming.  In 10th Symp. on Logic in Computer Science, D. Kozen, Ed. IEEE Computer Society Press, San Diego, California, 148–155.
  * Nadathur and Loveland (1998) Nadathur, G. and Loveland, D. W. 1998\.  Proof procedures for logic programming.  In Handbook of Logic in Artificial Intelligence and Logic Programming, D. M. Gabbay, C. J. Hogger, and J. A. Robinson, Eds. Vol. 5. Clarendon Press, Oxford, 163–234.
  * Nadathur and Miller (1988) Nadathur, G. and Miller, D. 1988\.  An Overview of $\lambda$Prolog.  In Fifth International Logic Programming Conference. MIT Press, Seattle, 810–827.
  * Nadathur and Miller (1990) Nadathur, G. and Miller, D. 1990\.  Higher-order Horn clauses.  J. of the ACM 37, 4, 777–814.
  * Nadathur and Mitchell (1999) Nadathur, G. and Mitchell, D. J. 1999\.  System description: Teyjus — A compiler and abstract machine based implementation of $\lambda$Prolog.  In 16th Conf. on Automated Deduction (CADE), H. Ganzinger, Ed. LNAI, vol. 1632. Springer, Trento, 287–291.
  * Nadathur and Pfenning (1992) Nadathur, G. and Pfenning, F. 1992\.  The type system of a higher-order logic programming language.  In Types in Logic Programming, F. Pfenning, Ed. MIT Press, 245–283.
  * Necula (1997) Necula, G. C. 1997\.  Proof-carrying code.  In Conference Record of the 24th Symposium on Principles of Programming Languages 97. ACM, Paris, France, 106–119.
  * Negri and von Plato (2001) Negri, S. and von Plato, J. 2001\.  Structural Proof Theory.  Cambridge University Press.
  * Nigam (2009) Nigam, V. 2009\.  Exploiting non-canonicity in the sequent calculus.  Ph.D. thesis, Ecole Polytechnique.
  * Nigam and Miller (2009) Nigam, V. and Miller, D. 2009\.  Algorithmic specifications in linear logic with subexponentials.  In ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP). ACM, 129–140.
  * Nigam et al. (2017) Nigam, V., Olarte, C., and Pimentel, E. 2017\.  On subexponentials, focusing and modalities in concurrent systems.  Theoretical Computer Science 693, 35–58.
  * Nigam et al. (2011) Nigam, V., Pimentel, E., and Reis, G. 2011\.  Specifying proof systems in linear logic with subexponentials.  In Proceedings of the Fifth Logical and Semantic Frameworks, with Applications Workshop (LSFA 2010). ENTCS, vol. 269. Elsevier, 109–123.
  * Nipkow (1993) Nipkow, T. 1993\.  Functional unification of higher-order patterns.  In 8th Symp. on Logic in Computer Science, M. Vardi, Ed. IEEE, 64–74.
  * O’Keefe (1990) O’Keefe, R. A. 1990\.  The Craft of Prolog.  MIT Press.
  * Olarte et al. (2015) Olarte, C., Nigam, V., and Pimentel, E. 2015\.  Subexponential concurrent constraint programming.  Theoretical Computer Science 606, 98–120.
  * Ono (1998) Ono, H. 1998\.  Proof-theoretic methods in nonclassical logic. an introduction.  In Theories of Types and Proofs, M. Takahashi, M. Okada, and M. Dezani-Ciancaglini, Eds. Mathematical Society of Japan Memoirs, vol. 2. Mathematical Society of Japan, 207–254.
  * Otten and Bibel (2003) Otten, J. and Bibel, W. 2003\.  leanCoP: lean connection-based theorem proving.  J. of Symbolic Computation 36, 1–2, 139–161.
  * Paulson (1989) Paulson, L. C. 1989\.  The foundation of a generic theorem prover.  J. of Automated Reasoning 5, 363–397.
  * Perlis (1982) Perlis, A. J. 1982\.  Epigrams on programming.  ACM SIGPLAN Notices 17, 9 (Sept.), 7–13.
  * Pettorossi and Proietti (1994) Pettorossi, A. and Proietti, M. 1994\.  Transformation of logic programs: Foundations and techniques.  J. of Logic Programming 19/20, 261–320.
  * Pfenning (1988) Pfenning, F. 1988\.  Partial polymorphic type inference and higher-order unification.  In Proceedings of the ACM Lisp and Functional Programming Conference. ACM.
  * Pfenning (1989) Pfenning, F. 1989\.  Elf: A language for logic definition and verified metaprogramming.  In 4th Symp. on Logic in Computer Science. IEEE, Monterey, CA, 313–321.
  * Pfenning (1991) Pfenning, F. 1991\.  Logic programming in the LF logical framework.  In Logical Frameworks, G. Huet and G. Plotkin, Eds. Cambridge University Press, 149–181.
  * Pfenning and Elliott (1988) Pfenning, F. and Elliott, C. 1988\.  Higher-order abstract syntax.  In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, 199–208.
  * Pfenning and Schürmann (1999) Pfenning, F. and Schürmann, C. 1999\.  System description: Twelf — A meta-logical framework for deductive systems.  In 16th Conf. on Automated Deduction (CADE), H. Ganzinger, Ed. LNAI, vol. 1632. Springer, Trento, 202–206.
  * Pientka (2002) Pientka, B. 2002\.  A proof-theoretic foundation for tabled higher-order logic programming.  In 18th International Conference on Logic Programming (ICLP 2002), P. J. Stuckey, Ed. LNCS, vol. 2401. Springer, 271–286.
  * Pitts (2003) Pitts, A. M. 2003\.  Nominal logic, A first order theory of names and binding.  Information and Computation 186, 2, 165–193.
  * Plotkin (1981) Plotkin, G. D. 1981\.  A structural approach to operational semantics.  DAIMI FN-19, Aarhus University, Aarhus, Denmark. Sept.
  * Plotkin (2004) Plotkin, G. D. 2004\.  A structural approach to operational semantics.  J. of Logic and Algebraic Programming 60-61, 17–139.
  * Polakow (2001) Polakow, J. 2001\.  Ordered linear logic and applications.  Ph.D. thesis, Department of Computer Science, Caregnie Mellon.
  * Polakow and Pfenning (1999) Polakow, J. and Pfenning, F. 1999\.  Natural deduction for intuitionistic non-commutative linear logic.  In Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications (TLCA’99), J.-Y. Girard, Ed. LNCS, vol. 1581. Springer, 295–309.
  * Pym and Harland (1994) Pym, D. and Harland, J. 1994\.  The uniform proof-theoretic foundation of linear logic programming.  J. of Logic and Computation 4, 2, 175–207.
  * Qi et al. (2015) Qi, X., Gacek, A., Holte, S., Nadathur, G., and Snow, Z. 2015\.  The Teyjus system – version 2.  http://teyjus.cs.umn.edu/.
  * Retoré (1997) Retoré, C. 1997\.  Pomset logic: a non-commutative extension of classical linear logic.  In Proceedings of TLCA. Vol. 1210. Springer, 300–318.
  * Robinson (1965) Robinson, J. A. 1965\.  A machine-oriented logic based on the resolution principle.  J. of the ACM 12, 23–41.
  * Ruet and Fages (1997) Ruet, P. and Fages, F. 1997\.  Concurrent constraint programming and non-commutative logic.  In Proceedings of the $11^{th}$ Conference on Computer Science Logic, M. Nielsen and W. Thomas, Eds. LNCS, vol. 1414. Springer.
  * Saraswat (1993) Saraswat, V. 1993\.  A brief introduction to linear concurrent constraint programming.  Tech. rep., Xerox Palo Alto Research Center.
  * Schroeder-Heister (1991) Schroeder-Heister, P. 1991\.  Uniform proof-theoretic semantics for logical constants (abstract).  J. of Symbolic Logic 56, 1142.
  * Schroeder-Heister (1993) Schroeder-Heister, P. 1993\.  Rules of definitional reflection.  In 8th Symp. on Logic in Computer Science, M. Vardi, Ed. IEEE Computer Society Press, IEEE, 222–232.
  * Schubert and Urzyczyn (2018) Schubert, A. and Urzyczyn, P. 2018\.  First-order answer set programming as constructive proof search.  Theory Pract. Log. Program. 18, 3-4, 673–690.
  * Schwichtenberg (2006) Schwichtenberg, H. 2006\.  Minlog.  In The Seventeen Provers of the World, F. Wiedijk, Ed. LNCS, vol. 3600. Springer, 151–157.
  * Scott (1970) Scott, D. 1970\.  Outline of a mathematical theory of computation.  In Proceedings, 4th Annual Princeton Conference on Information Sciences and Systems. Princeton University, 169–176.  Also, Programming Research Group Technical Monograph PRG–2, Oxford University.
  * Simmons and Pfenning (2008) Simmons, R. J. and Pfenning, F. 2008\.  Linear logical algorithms.  In 35th International Colloquium Automata, Languages and Programming (ICALP 2008), L. Aceto, I. Damgård, L. A. Goldberg, M. M. Halldórsson, A. Ingólfsdóttir, and I. Walukiewicz, Eds. LNCS, vol. 5126. Springer, 336–347.
  * Sørensen and Urzyczyn (2006) Sørensen, M. H. and Urzyczyn, P. 2006\.  Lectures on the Curry-Howard Isomorphism. Studies in Logic, vol. 149.  Elsevier.
  * Stampoulis and Chlipala (2018) Stampoulis, A. and Chlipala, A. 2018\.  Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of $\lambda$Prolog/Makam.  Proc. ACM Program. Lang. 2, ICFP, 93:1–93:30.
  * Statman (1979) Statman, R. 1979\.  Intuitionistic propositional logic is polynomial-space complete.  Theoretical Computer Science 9, 67–72.
  * Stickel (1988) Stickel, M. 1988\.  A PROLOG technology theorem prover: Implementation by an extended PROLOG compiler.  J. of Automated Reasoning 4, 4, 353–380.
  * Stoy (1977) Stoy, J. E. 1977\.  Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory.  MIT Press, Cambridge, MA.
  * Takahashi (1967) Takahashi, M. 1967\.  A proof of cut-elimination theorem in simple type theory.  J. of the Mathematical Society of Japan 19, 399–410.
  * Takeuti (1953) Takeuti, G. 1953\.  On a generalized logic calculus.  Japanese Journal of Mathematics 23, 39–96.  Errata: ibid, vol. 24 (1954), 149–156.
  * Tärnlund (1977) Tärnlund, S.-A. 1977\.  Horn Clause Computability.  BIT 17, 215–226.
  * Tassi (2018) Tassi, E. 2018\.  Elpi: an extension language for Coq.  CoqPL 2018: The Fourth International Workshop on Coq for Programming Languages.
  * Tassi (2019) Tassi, E. 2019\.  Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq.  In 10th International Conference on Interactive Theorem Proving (ITP 2019), J. Harrison, J. O’Leary, and A. Tolmach, Eds. Leibniz International Proceedings in Informatics (LIPIcs), vol. 141. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 29:1–29:18.
  * Van Gelder et al. (1991) Van Gelder, A., Ross, K. A., and Schilpf, J. S. 1991\.  The well-founded semantics for general logic programs.  J. of the ACM 38, 3, 620–662.
  * Wadge (1991) Wadge, W. W. 1991\.  Higher-order Horn logic programming.  In Proceedings of the 1991 International Symposium on Logic Programming. MIT Press, San Diego, California, USA, 289–303.
  * Wadler (2003) Wadler, P. 2003\.  Call-by-value is dual to call-by-name.  In 8th Int. Conf. on Functional Programming. ACM, New York, NY, 189–201.
  * Wang (2016) Wang, Y. 2016\.  A higher-order abstract syntax approach to the verified compilation of functional programs.  Ph.D. thesis, University of Minnesota.
  * Wang and Nadathur (2016) Wang, Y. and Nadathur, G. 2016\.  A higher-order abstract syntax approach to verified transformations on functional programs.  In Programming Languages and Systems. ESOP 2016, P. Thiemann, Ed. LNCS, vol. 9632. Springer, 752–779.
  * Wansing (2002) Wansing, H. 2002\.  Sequent systems for modal logics.  In Handbook of Philosophical Logic, Volume VIII, 2 ed., D. M. Gabbay and F. Guenthner, Eds. Kluwer Academic Publishers, Amsterdam, 61–146.
  * Warren (1982) Warren, D. H. D. 1982\.  Higher-order extensions to Prolog: Are they needed?  In Machine Intelligence 10. Halsted Press, Chicester, England, 441–454.
  * Warren (1983) Warren, D. H. D. 1983\.  An abstract Prolog instruction set.  Tech. Rep. 309, SRI International.
  * Warren (2018) Warren, D. S. 2018\.  Top-down and Bottom-up Evaluation Procedurally Integrated.  Theory Pract. Log. Program 18, 3-4, 706–721.
  * Whalen (2005) Whalen, M. W. 2005\.  Trustworthy translation for the requirements state machine language without events.  Ph.D. thesis, University of Minnesota.
  * Wielemaker et al. (2012) Wielemaker, J., Schrijvers, T., Triska, M., and Lager, T. 2012\.  SWI-Prolog.  Theory Pract. Log. Program 12, 1-2, 67–96.
  * Wos and McCune (1991) Wos, L. and McCune, W. 1991\.  Automated theorem proving and logic programming: A natural symbiosis.  J. of Logic Programming 11, 1–53.
  * Zamov and Sharonov (1971) Zamov, N. K. and Sharonov, V. I. 1971\.  On a class of strategies for the resolution method.  In Studies in Constructive Mathematics and Mathematical Logic, Part III, A. O. Slisenko, Ed. Number 16 in Seminars in Mathematics, V.A. Steklov Mathematical Institute, Leningrad. Consultants Bureau, New York, 26–31.  Translated from Russian by J. S. Wood.