Term Rewriting and all That, 1998. ,
JTS: tools for implementing domain-specific languages, Proceedings. Fifth International Conference on Software Reuse (Cat. No.98TB100203), pp.143-153, 1998. ,
DOI : 10.1109/ICSR.1998.685739
Automated correctness proofs of machine code programs for a commercial microprocessor, Proceedings of the Eleventh International Conference on Automated Deduction, pp.416-430, 1992. ,
Matching Power, Proceedings of RTA'2001, 2001. ,
DOI : 10.1007/3-540-45127-7_8
URL : https://hal.archives-ouvertes.fr/inria-00099308
Zenon: an automatic theorem prover for first-order logic Available as part of the Focal system at http ,
Theorem proving modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003. ,
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/hal-01199506
Optimizing pattern matching, Proceedings of the sixth ACM SIGPLAN International Conference on Functional Programming, pp.26-37, 2001. ,
Global value numbering using random interpretation, POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.342-352, 2004. ,
Natural semantics, 4th Annual Symposium on Theoretical Aspects of Computer Sciences on STACS 87, pp.22-39, 1987. ,
DOI : 10.1007/BFb0039592
URL : https://hal.archives-ouvertes.fr/inria-00075953
Promoting rewriting to a programming language: A compiler for non-deterministic rewrite programs in associative-commutative theories, Journal of Functional Programming, vol.11, issue.2, pp.207-251, 2001. ,
On extending Java, Proceedings of the Joint Modular Languages Conference on Modular Programming Languages, pp.321-335, 1997. ,
DOI : 10.1007/3-540-62599-2_49
Proving correctness of compiler optimizations by temporal logic, Proc. 29th ACM Symposium on Principles of Programming Languages, pp.283-294, 2002. ,
Correctness of a compiler for arithmetic expressions A Pattern Matching Compiler for Multiple Target Languages, Proceedings Symposium in Applied Mathematics 12th Conference on Compiler Construction, pp.33-41, 1967. ,
Advice on structuring compilers and proving them correct, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '73, pp.144-152, 1973. ,
DOI : 10.1145/512927.512941
Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.106-119, 1997. ,
The design and implementation of a certifying compiler, SIGPLAN Not, vol.39, issue.4, pp.612-625, 2004. ,
The VLISP verified PreScheme compiler, LISP and Symbolic Computation, vol.57, issue.2?3, pp.111-182, 1995. ,
DOI : 10.1007/BF01128408
Translation validation, Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, pp.151-166, 1998. ,
DOI : 10.1007/BFb0054170
Credible compilation with pointers, Proceedings of the FLoC Workshop on Run-Time Result Verification, 1999. ,
Symbolic transfer function-based approaches to certified compilation, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.1-13, 2004. ,
Generator of efficient strongly typed abstract syntax trees in Java, IEE Proceedings - Software Engineering, pp.70-79, 2005. ,
Views: a way for pattern matching to cohabit with data abstraction, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '87, pp.307-313, 1987. ,
DOI : 10.1145/41625.41653
Foundational proof checkers with small witnesses, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming , PPDP '03, pp.264-274, 2003. ,
DOI : 10.1145/888251.888276