Formal validation of pattern matching code

DOI10.4230/OASICS.TRUSTWORTHYSW.2006.697MaRDI QIDQ2917405zbMATH OpenOpenAlexFDO

Authors Claude Kirchner, Pierre-Etienne Moreau, Antoine Reilles

Publication date 28 September 2012

Full work available at URL https://dblp.uni-trier.de/db/conf/dagstuhl/P6000.html#KirchnerMR06

zbMATH Keywords

compilerscorrectness proofspattern matchingvalidation

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• The code validation tool (CVT). Automatic verification of a compilation process
• Compiling regular patterns
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Formal verification of translation validators
• Semantics-directed compilation of nonlinear patterns

Cited in

(4)

• The code validation tool (CVT). Automatic verification of a compilation process
• Canonical abstract syntax trees
• Translation Correctness for First-Order Object-Oriented Pattern Matching
• A \(\rho\)-calculus of explicit constraint application

Describes a project that uses

Uses Software

• ML
• CHEVIE

This page was built for publication: Formal validation of pattern matching code

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2917405)