Proof contexts with late binding

DOI10.1007/11417170_24MaRDI QIDQ5704019zbMATH OpenOpenAlexFDO

Authors Virgile Prevosto, Sylvain Boulmé

Publication date 11 November 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b135690

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Symbolic computation and algebraic computation (68W30)

Recommendations

• Focusing and higher-order abstract syntax
• Algorithms and proofs inheritance in the FOC language
• Engineering formal metatheory
• Theorem-proving support in programming language semantics
• Meta-theory à la carte

Cited in

(2)

• Invariants for the FoCaL language
• ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Proof contexts with late binding

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