scientific article; zbMATH DE number 5033848

MaRDI QIDQ5472887zbMATH OpenFDO

Authors Mark-Oliver Stehr

Publication date 19 June 2006

zbMATH Keywords

equational specificationrewriting logictype theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Second- and higher-order arithmetic and fragments (03F35) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Pure type systems in rewriting logic: specifying typed higher-order languages in a first-order logical framework
• scientific article; zbMATH DE number 5033853
• Variants of the basic calculus of constructions
• scientific article; zbMATH DE number 4014064
• A simple model construction for the calculus of constructions
• Type checking with universes
• scientific article; zbMATH DE number 3928956
• Definitions by rewriting in the Calculus of Constructions
• scientific article; zbMATH DE number 4191621
• A higher-order calculus and theory abstraction

Cited in

(4)

• Twenty years of rewriting logic
• scientific article; zbMATH DE number 5033853 (Why is no real title available?)
• Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
• Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types

This page was built for publication:

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