A dependently typed multi-stage calculus

DOI10.1007/978-3-030-34175-6_4MaRDI QIDQ6536307zbMATH OpenFDO

Authors Akira Kawata, Atsushi Igarashi

Publication date 19 April 2024

zbMATH Keywords

dependent typescross-stage persistencemulti-stage programming

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Recommendations

• On Cross-Stage Persistence in Multi-Stage Programming
• MetaML and multi-stage programming with explicit annotations
• Tagless staged interpreters for typed languages
• Reasoning about multi-stage programs
• Staged computation with staged lexical scope

Cites work

• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• A Logical Foundation for Environment Classifiers
• A framework for defining logics
• A modal analysis of staged computation
• A polymorphic modal type system for Lisp-like multi-staged languages
• A theory of type polymorphism in programming
• A type system for certified binaries
• Environment classifiers
• Guarded recursive datatype constructors
• Meta-programming through typeful code representation
• MetaML and multi-stage programming with explicit annotations
• On Cross-Stage Persistence in Multi-Stage Programming
• Program logics for homogeneous generative run-time meta-programming
• Staged computation with names and necessity
• Tagless staged interpreters for typed languages
• The calculus of constructions
• Types and programing languages

This page was built for publication: A dependently typed multi-stage calculus

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