Proof pearl: Abella formalization of lambda calculus cube property, Second International Conference on Certified Programs and Proofs, vol.7679, pp.173-187, 2012. ,
Logic Programming with Focusing Proofs in Linear Logic, J. of Logic and Computation, vol.2, pp.297-347, 1992. ,
Contributions to the theory of logic programming, JACM, vol.29, pp.841-862, 1982. ,
Intrinsically-typed Definitional Interpreters for Imperative Languages, Proc. ACM Program. Lang. 2, POPL, vol.34, p.16, 2017. ,
Least and greatest fixed points in linear logic, ACM Trans. on Computational Logic, vol.13, 2012. ,
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
The Bedwyr system for model checking over syntactic expressions, 21th Conf. on Automated Deduction (CADE) (LNAI), F. Pfenning, pp.391-397, 2007. ,
Automatic Proof and Disproof in Isabelle/HOL, FroCoS (Lecture Notes in Computer Science, vol.6989, pp.12-27, 2011. ,
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
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
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. ,
2017. ? Check: A mechanized metatheory model checker, Theory and Practice of Logic Programming, vol.17, pp.311-352, 2017. ,
Advances in Property-Based Testing for ? Prolog, Tests and Proofs -10th International Conference, vol.9762, pp.37-56, 2016. ,
A semantic framework for proof evidence, J. of Automated Reasoning, vol.59, pp.287-330, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01390912
Generating constrained random data with uniform distribution, J. Funct. Program, vol.25, 2015. ,
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. ,
Negation as failure. In Logic and Data Bases, pp.293-322, 1978. ,
ELPI: Fast, Embeddable, ?Prolog Interpreter, Proceedings of LPAR. Suva, Fiji, 2015. ,
Feat: functional enumeration of algebraic types, pp.61-72, 2012. ,
Semantics Engineering with PLT Redex, 2009. ,
Hybrid -A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax, J. Autom. Reasoning, vol.48, pp.43-105, 2012. ,
Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System, ESOP, vol.9032, pp.383-405, 2015. ,
Inference and learning in probabilistic logic programs using weighted Boolean formulas, TPLP, vol.15, pp.358-401, 2015. ,
Combining generic judgments with recursive definitions, 23th Symp. on Logic in Computer Science, F. Pfenning, pp.33-44, 2008. ,
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
Investigations into Logical Deduction, The Collected Papers of Gerhard, pp.68-131, 1935. ,
, Linear Logic. Theoretical Computer Science, vol.50, pp.1-102, 1987.
An email posting to the mailing list linear@cs, 1992. ,
A Proof Theory for Model Checking: An Extended Abstract, Proceedings Fourth International Workshop on Linearity, vol.238, 2017. ,
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. ,
QuickCheck Testing for Fun and Profit, Practical Aspects of Declarative Languages, 9th International Symposium, vol.4354, pp.1-32, 2007. ,
Productive use of failure in inductive proof, Journal of Automated Reasoning, vol.16, pp.79-111, 1996. ,
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. ,
Beginner's Luck: A Language for Random Generators, 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL, 2017. ,
Focusing and Polarization in Linear, Intuitionistic, and Classical Logics, Theoretical Computer Science, vol.410, pp.4747-4768, 2009. ,
Cut-elimination for a logic with definitions and induction, Theoretical Computer Science, vol.232, pp.171-172, 2000. ,
Reasoning with Higher-Order Abstract Syntax in a Logical Framework, ACM Trans. on Computational Logic, vol.3, pp.80-136, 2002. ,
Encoding transition systems in sequent calculus, Theoretical Computer Science, vol.294, pp.411-437, 2003. ,
Effect-driven QuickChecking of compilers, PACMPL, vol.1, pp.1-15, 2017. ,
Mechanized Metatheory Revisited, Journal of Automated Reasoning, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01884210
Programming with Higher-Order Logic, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00776197
Uniform Proofs as a Foundation for Logic Programming, Annals of Pure and Applied Logic, vol.51, pp.125-157, 1991. ,
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
A proof theory for generic judgments, ACM Trans. on Computational Logic, vol.6, pp.749-783, 2005. ,
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. ,
The type system of a higher-order logic programming language, Types in Logic Programming, Frank Pfenning, pp.245-283, 1992. ,
Applications of Foundational Proof Certificates in theorem proving, Ph.D. Dissertation, 2017. ,
URL : https://hal.archives-ouvertes.fr/tel-01743857
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. ,
Foundational Property-Based Testing, Interactive Theorem Proving -6th International Conference, vol.2015, pp.325-343, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01162898
Online Justification for Tabled Logic Programs, 2004. ,
, , pp.24-38
System Description: Twelf -A Meta-Logical Framework for Deductive Systems, 16th Conf. on Automated Deduction (CADE) (LNAI), H. Ganzinger, pp.202-206, 1999. ,
Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description), Fifth International Joint Conference on Automated Reasoning, pp.15-21, 2010. ,
Operationally Based Theories of Program Equivalence, Semantics and Logics of Computation, 1997. ,
Smallcheck and Lazy Smallcheck: automatic exhaustive testing for small values, pp.37-48, 2008. ,
Tor: Modular search with hookable disjunction, Sci. Comput. Program, vol.84, pp.101-120, 2014. ,
Definitional Reflection and the Completion, Proceedings of the 4th International Workshop on Extensions of Logic Programming, vol.798, pp.333-347, 1993. ,
Rules of Definitional Reflection, 8th Symp. on Logic in Computer Science, pp.222-232, 1993. ,
Proof Search Specifications of Bisimulation and Modal Logics for the ? -calculus, ACM Trans. on Computational Logic, vol.11, pp.1-13, 2010. ,