Reasoning about multi-stage programs

DOI10.1017/S0956796816000253zbMath1420.68040MaRDI QIDQ5371979

Walid Taha, Jun-ichiro Inoue

Publication date: 23 October 2017

Published in: Journal of Functional Programming (Search for Journal in Brave)

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Galois connecting call-by-value and call-by-name

Uses Software

• LMS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the semantics of the bad-variable constructor in Algol-like languages
• Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code
• A new approach to abstract syntax with variable binding
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Fully abstract models of typed \(\lambda\)-calculi
• On abstraction and the expressive power of programming languages
• Bisimilarity as a theory of functional programming
• Proving congruence of bisimulation in functional programming languages
• In search of a program generator to implement generic transformations for high-performance computing
• Combining partial evaluation and staged interpretation in the implementation of domain-specific languages
• Reasoning about Multi-stage Programs
• Shifting the stage
• Environment classifiers
• Engineering formal metatheory
• A Lambda-Calculus with Constructors
• The Omega Rule is $\mathbf{\Pi_{1}^{1}}$-Complete in the $\lambda\beta$-Calculus
• Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
• The λ-calculus is ω-incomplete
• Full Abstraction and the Context Lemma
• Size-Change Termination and Transition Invariants
• Equivalence in functional languages with effects
• A fresh look at programming with names and binders
• Program Logics for Homogeneous Generative Run-Time Meta-Programming
• Contextual modal type theory
• Small bisimulations for reasoning about higher-order imperative programs
• A polymorphic modal type system for lisp-like multi-staged languages
• Static analysis of multi-staged programs via unstaging translation
• Enhancements of the bisimulation proof method
• A Logical Foundation for Environment Classifiers
• Parallel reductions in \(\lambda\)-calculus

This page was built for publication: Reasoning about multi-stage programs