Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
From MaRDI portal
Publication:3644934
DOI10.1017/S0956796809007205zbMath1191.68158OpenAlexW2123092976WikidataQ60712738 ScholiaQ60712738MaRDI QIDQ3644934
Jacques Carette, Chung-Chieh Shan, Oleg Kiselyov
Publication date: 13 November 2009
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0956796809007205
Related Items (16)
Finally tagless observable recursion for an abstract grammar model ⋮ Generating C. System description ⋮ Unified program generation and verification: a case study on number-theoretic transform ⋮ Functional un\(|\)unparsing ⋮ Deep embedding with class ⋮ Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala ⋮ Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library ⋮ Reasoning about multi-stage programs ⋮ The calculus of dependent lambda eliminations ⋮ Query lifting. Language-integrated query for heterogeneous nested collections ⋮ Combining deep and shallow embedding of domain-specific languages ⋮ Functional Semantics ⋮ Incorporating quotation and evaluation into Church's type theory ⋮ Probabilistic Inference by Program Transformation in Hakaru (System Description) ⋮ Declarative Foreign Function Binding Through Generic Programming ⋮ Language-integrated query with nested data structures and grouping
Cites Work
- Notions of computation and monads
- Automatic synthesis of typed \(\Lambda\)-programs on term algebras
- Strictness analysis and denotational abstract interpretation
- Metacircularity in the polymorphic \(\lambda\)-calculus
- Automatic autoprojection of recursive equations with global variables and abstract data types
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- LCF considered as a programming language
- A theory of type polymorphism in programming
- Encoding types in ML-like languages
- Type-indexed data types
- Environment classifiers
- Guarded recursive datatype constructors
- Typing dynamic typing
- Meta-programming with names and necessity
- A modal analysis of staged computation
- Embedded interpreters
- Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums
- Two-Level Functional Languages
- Coinductive characterizations of applicative structures
- Efficient self-interpretation in lambda calculus
- A partial evaluator for the untyped lambda-calculus
- Combinators for program generation
- Contextual modal type theory
- Typed cross-module compilation
- Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism
- The next 700 programming languages
- The Principal Type-Scheme of an Object in Combinatory Logic
- Staged computation with names and necessity
- Binding-time analysis for both static and dynamic expressions
- A hybrid approach to online and offline partial evaluation
This page was built for publication: Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
