Imperative LF Meta-Programming

DOI10.1016/j.entcs.2007.11.017zbMath1278.03067OpenAlexW2132259423MaRDI QIDQ2871844

Aaron Stump

Publication date: 10 January 2014

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2007.11.017

zbMATH Keywords

logical frameworksmeta-programmingrewriting calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• Twelf
• ALF
• CVC
• Cayenne
• MicroRogue

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Dependently typed records in type theory
• A syntactic approach to foundational proof-carrying code
• A language-based approach to functionally correct imperative programming
• Pure patterns type systems
• A framework for defining logics
• Dependent types ensure partial correctness of theorem provers
• Cayenne—a language with dependent types

This page was built for publication: Imperative LF Meta-Programming