. Beniamino-accattoli, Proof pearl: Abella formalization of lambda calculus cube property, Second International Conference on Certified Programs and Proofs, vol.7679, pp.173-187, 2012.

J. Andreoli, Logic Programming with Focusing Proofs in Linear Logic, J. of Logic and Computation, vol.2, pp.297-347, 1992.

K. R. Apt and M. H. Van-emden, Contributions to the theory of logic programming, JACM, vol.29, pp.841-862, 1982.

C. Bach-poulsen, A. Rouvoet, A. Tolmach, R. Krebbers, and E. Visser, Intrinsically-typed Definitional Interpreters for Imperative Languages, Proc. ACM Program. Lang. 2, POPL, vol.34, p.16, 2017.

D. Baelde, Least and greatest fixed points in linear logic, ACM Trans. on Computational Logic, vol.13, 2012.

D. Baelde, K. Chaudhuri, A. Gacek, D. Miller, G. Nadathur et al., Abella: A System for Reasoning about Relational Specifications, Journal of Formalized Reasoning, vol.7, issue.2, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102709

D. Baelde, A. Gacek, D. Miller, G. Nadathur, and A. Tiu, The Bedwyr system for model checking over syntactic expressions, 21th Conf. on Automated Deduction (CADE) (LNAI), F. Pfenning, pp.391-397, 2007.

. Jasmin-christian, L. Blanchette, T. Bulwahn, and . Nipkow, Automatic Proof and Disproof in Isabelle/HOL, FroCoS (Lecture Notes in Computer Science, vol.6989, pp.12-27, 2011.

R. Blanco, Z. Chihani, and D. Miller, Translating Between Implicit and Explicit Versions of Proof, Automated Deduction -CADE 26 -26th International Conference on Automated Deduction, vol.10395, pp.255-273, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01645016

R. Blanco and D. Miller, Proof Outlines as Proof Certificates: a system description, Proceedings First International Workshop on Focusing (Electronic Proceedings in Theoretical Computer Science), vol.197, pp.7-14, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01238436

L. Bulwahn, The New Quickcheck for Isabelle -Random, Exhaustive and Symbolic Testing under One Roof, Certified Programs and Proofs -Second International Conference, vol.2012, pp.92-108, 2012.

J. Cheney and A. Momigliano, 2017. ? Check: A mechanized metatheory model checker, Theory and Practice of Logic Programming, vol.17, pp.311-352, 2017.

J. Cheney, A. Momigliano, and M. Pessina, Advances in Property-Based Testing for ? Prolog, Tests and Proofs -10th International Conference, vol.9762, pp.37-56, 2016.

Z. Chihani, D. Miller, and F. Renaud, A semantic framework for proof evidence, J. of Automated Reasoning, vol.59, pp.287-330, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01390912

K. Claessen, J. Duregård, and M. H. Palka, Generating constrained random data with uniform distribution, J. Funct. Program, vol.25, 2015.

K. Claessen and J. Hughes, QuickCheck: a lightweight tool for random testing of Haskell programs, Proceedings of the 2000 ACM SIGPLAN International Conference on Functional Programming, pp.268-279, 2000.

K. L. Clark, Negation as failure. In Logic and Data Bases, pp.293-322, 1978.

C. Dunchev, F. Guidi, C. Sacerdoti-coen, and E. Tassi, ELPI: Fast, Embeddable, ?Prolog Interpreter, Proceedings of LPAR. Suva, Fiji, 2015.

J. Duregård, P. Jansson, and M. Wang, Feat: functional enumeration of algebraic types, pp.61-72, 2012.

M. Felleisen, R. B. Findler, and M. Flatt, Semantics Engineering with PLT Redex, 2009.

A. P. Felty and A. Momigliano, Hybrid -A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax, J. Autom. Reasoning, vol.48, pp.43-105, 2012.

B. Fetscher, K. Claessen, M. H. Palka, J. Hughes, and R. B. Findler, Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System, ESOP, vol.9032, pp.383-405, 2015.

D. Fierens, G. Van-den, J. Broeck, D. Renkens, . Sht et al., Inference and learning in probabilistic logic programs using weighted Boolean formulas, TPLP, vol.15, pp.358-401, 2015.

A. Gacek, D. Miller, and G. Nadathur, Combining generic judgments with recursive definitions, 23th Symp. on Logic in Computer Science, F. Pfenning, pp.33-44, 2008.

A. Gacek, D. Miller, and G. Nadathur, A two-level logic approach to reasoning about computations, J. of Automated Reasoning, vol.49, pp.241-273, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00776208

G. Gentzen, Investigations into Logical Deduction, The Collected Papers of Gerhard, pp.68-131, 1935.

J. Girard, Linear Logic. Theoretical Computer Science, vol.50, pp.1-102, 1987.

J. Girard, An email posting to the mailing list linear@cs, 1992.

Q. Heath and D. Miller, A Proof Theory for Model Checking: An Extended Abstract, Proceedings Fourth International Workshop on Linearity, vol.238, 2017.

C. Hritcu, J. Hughes, and B. C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, and Leonidas Lampropoulos, Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP '13), pp.455-468, 2013.

J. Hughes, QuickCheck Testing for Fun and Profit, Practical Aspects of Declarative Languages, 9th International Symposium, vol.4354, pp.1-32, 2007.

A. Ireland and A. Bundy, Productive use of failure in inductive proof, Journal of Automated Reasoning, vol.16, pp.79-111, 1996.

C. Klein, J. Clements, C. Dimoulas, C. Eastlund, M. Felleisen et al., Run your research: on the effectiveness of lightweight mechanization, Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '12), pp.285-296, 2012.

L. Lampropoulos, D. Gallois-wong, C. Hri?cu, J. Hughes, B. C. Pierce et al., Beginner's Luck: A Language for Random Generators, 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL, 2017.

C. Liang and D. Miller, Focusing and Polarization in Linear, Intuitionistic, and Classical Logics, Theoretical Computer Science, vol.410, pp.4747-4768, 2009.

R. Mcdowell and D. Miller, Cut-elimination for a logic with definitions and induction, Theoretical Computer Science, vol.232, pp.171-172, 2000.

R. Mcdowell and D. Miller, Reasoning with Higher-Order Abstract Syntax in a Logical Framework, ACM Trans. on Computational Logic, vol.3, pp.80-136, 2002.

R. Mcdowell, D. Miller, and C. Palamidessi, Encoding transition systems in sequent calculus, Theoretical Computer Science, vol.294, pp.411-437, 2003.

J. Midtgaard, M. N. Justesen, P. Kasting, F. Nielson, and H. Nielson, Effect-driven QuickChecking of compilers, PACMPL, vol.1, pp.1-15, 2017.

D. Miller, Mechanized Metatheory Revisited, Journal of Automated Reasoning, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01884210

D. Miller and G. Nadathur, Programming with Higher-Order Logic, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00776197

D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov, Uniform Proofs as a Foundation for Logic Programming, Annals of Pure and Applied Logic, vol.51, pp.125-157, 1991.

D. Miller and A. Saurin, A Game Semantics for Proof Search: Preliminary Results, Electr. Notes Theor. Comput. Sci, vol.155, pp.543-563, 2006.
URL : https://hal.archives-ouvertes.fr/hal-00527881

D. Miller and A. Tiu, A proof theory for generic judgments, ACM Trans. on Computational Logic, vol.6, pp.749-783, 2005.

A. Momigliano, A supposedly fun thing i may have to do again: a HOAS encoding of Howe's method, Proceedings of the seventh international workshop on Logical frameworks and meta-languages, theory and practice (LFMTP '12), pp.33-42, 2012.

G. Nadathur and F. Pfenning, The type system of a higher-order logic programming language, Types in Logic Programming, Frank Pfenning, pp.245-283, 1992.

R. Blanco and M. , Applications of Foundational Proof Certificates in theorem proving, Ph.D. Dissertation, 2017.
URL : https://hal.archives-ouvertes.fr/tel-01743857

M. H. Palka, K. Claessen, A. Russo, and J. Hughes, Testing an optimising compiler by generating random lambda terms, Proceedings of the 6th International Workshop on Automation of Software Test, AST 2011, pp.91-97, 2011.

Z. Paraskevopoulou, C. Hritcu, M. Dénès, L. Lampropoulos, and B. C. Pierce, Foundational Property-Based Testing, Interactive Theorem Proving -6th International Conference, vol.2015, pp.325-343, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01162898

G. Pemmasani, H. Guo, Y. Dong, C. R. Ramakrishnan, and I. V. Ramakrishnan, Online Justification for Tabled Logic Programs, 2004.

H. Springer-berlin, , pp.24-38

F. Pfenning and C. Schürmann, System Description: Twelf -A Meta-Logical Framework for Deductive Systems, 16th Conf. on Automated Deduction (CADE) (LNAI), H. Ganzinger, pp.202-206, 1999.

B. Pientka and J. Dunfield, Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description), Fifth International Joint Conference on Automated Reasoning, pp.15-21, 2010.

A. M. Pitts, Operationally Based Theories of Program Equivalence, Semantics and Logics of Computation, 1997.

C. Runciman, M. Naylor, and F. Lindblad, Smallcheck and Lazy Smallcheck: automatic exhaustive testing for small values, pp.37-48, 2008.

T. Schrijvers, B. Demoen, M. Triska, and B. Desouter, Tor: Modular search with hookable disjunction, Sci. Comput. Program, vol.84, pp.101-120, 2014.

P. Schroeder-heister, Definitional Reflection and the Completion, Proceedings of the 4th International Workshop on Extensions of Logic Programming, vol.798, pp.333-347, 1993.

P. Schroeder-heister, Rules of Definitional Reflection, 8th Symp. on Logic in Computer Science, pp.222-232, 1993.

A. Tiu and D. Miller, Proof Search Specifications of Bisimulation and Modal Logics for the ? -calculus, ACM Trans. on Computational Logic, vol.11, pp.1-13, 2010.