D. Baelde, Least and greatest fixed points in linear logic, ACM Trans. on Computational Logic, vol.13, issue.1, 2012.
DOI : 10.1007/978-3-540-75560-9_9
URL : http://arxiv.org/pdf/0910.3383

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), number 4603 in LNAI, pp.391-397, 2007.
DOI : 10.1007/978-3-540-73595-3_28

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, p.2014
URL : https://hal.archives-ouvertes.fr/hal-01102709

J. C. Blanchette, L. Bulwahn, and T. Nipkow, Automatic Proof and Disproof in Isabelle/HOL, FroCoS, pp.12-27, 2011.
DOI : 10.1007/BFb0028402
URL : http://www4.in.tum.de/%7Eblanchet/frocos2011-dis-proof.pdf

R. Blanco and D. Miller, Proof Outlines as Proof Certificates: A System Description, Electronic Proceedings in Theoretical Computer Science, vol.2758, issue.2
DOI : 10.1007/10930755_8
URL : https://hal.archives-ouvertes.fr/hal-01238436

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, pp.255-273, 2017.
DOI : 10.1017/CBO9781139168717
URL : https://hal.archives-ouvertes.fr/hal-01645016

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

J. Cheney, A. Momigliano, and M. Pessina, Advances in Property-Based Testing for $$\alpha $$ Prolog, Tests and Proofs -10th International Conference Proceedings, volume 9762 of Lecture Notes in Computer Science, pp.37-56, 2016.
DOI : 10.1145/1993498.1993532
URL : http://arxiv.org/pdf/1604.08345

Z. Chihani, D. Miller, and F. Renaud, A Semantic Framework for Proof Evidence, Journal of Automated Reasoning, vol.42, issue.1, 2016.
DOI : 10.1017/CBO9781139168717
URL : https://hal.archives-ouvertes.fr/hal-01390912

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.

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

A. Gacek, D. Miller, and G. Nadathur, Combining Generic Judgments with Recursive Definitions, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pp.33-44, 2008.
DOI : 10.1109/LICS.2008.33
URL : http://arxiv.org/pdf/0802.0865

Q. Heath and D. Miller, A Proof Theory for Model Checking: An Extended Abstract, Proceedings Fourth International Workshop on Linearity, 2016.
DOI : 10.1016/j.jal.2012.07.007
URL : http://arxiv.org/pdf/1701.04915

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.

C. Liang and D. Miller, Focusing and polarization in linear, intuitionistic, and classical logics, Theoretical Computer Science, vol.410, issue.46, pp.4747-4768, 2009.
DOI : 10.1016/j.tcs.2009.07.041
URL : https://doi.org/10.1016/j.tcs.2009.07.041

R. Mcdowell, D. Miller, and G. Nadathur, Reasoning with higher-order abstract syntax in a logical framework Programming with Higher-Order Logic, ACM Trans. on Computational Logic, vol.317, issue.1, pp.80-136, 2002.

D. Miller and A. Tiu, A proof theory for generic judgments, ACM Transactions on Computational Logic, vol.6, issue.4, pp.749-783, 2005.
DOI : 10.1145/1094622.1094628
URL : http://www.cse.psu.edu/~dale/papers/nabla-subm.pdf

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, issue.1-2, pp.125-157, 1991.
DOI : 10.1016/0168-0072(91)90068-W
URL : https://doi.org/10.1016/0168-0072(91)90068-w

G. Nadathur and D. J. Mitchell, System Description: Teyjus???A Compiler and Abstract Machine Based Implementation of ??Prolog, 16th Conf. on Automated Deduction (CADE), number 1632 in LNAI, pp.287-291, 1999.
DOI : 10.1007/3-540-48660-7_25

L. Naish, A declarative debugging scheme, Journal of Functional and Logic Programming, issue.3, 1997.
DOI : 10.1109/acsc.2000.824398
URL : http://www.cs.tu-berlin.de/journal/jflp/articles/1997/A97-03/JFLP-A97-03.ps.gz

Z. Paraskevopoulou, C. Hritcu, M. Dénès, L. Lampropoulos, and B. C. Pierce, Foundational Property-Based Testing, Interactive Theorem Proving -6th International Conference, ITP 2015, Proceedings, pp.325-343, 2015.
DOI : 10.1007/978-3-319-22102-1_22
URL : https://hal.archives-ouvertes.fr/hal-01162898