A modal analysis of staged computation
From MaRDI portal
Recommendations
Cited in
(90)- A proof-theoretic investigation of a logic of positions
- MetaML and multi-stage programming with explicit annotations
- Intensional computation with higher-order functions
- Fibrational modal type theory
- Incorporating quotation and evaluation into Church's type theory
- Classical natural deduction for S4 modal logic
- Encoding types in ML-like languages
- Pattern matching as cut elimination
- Type-specialized staged programming with process separation
- Subatomic natural deduction for a naturalistic first-order language with non-primitive identity
- Self-quotation in a typed, intensional lambda-calculus
- Nested sequents for intuitionistic modal logics via structural refinement
- Game semantics for constructive modal logic
- Semantical analysis of contextual types
- Dual and axiomatic systems for constructive S4, a formally verified equivalence
- Hypothetical logic of proofs
- Harmony in multiple-conclusion natural-deduction
- Connectionist computations of intuitionistic reasoning
- A general method for proving decidability of intuitionistic modal logics
- A framework for intuitionistic grammar logics
- Domain-free -calculus
- Intuitionistic hypothetical logic of proofs
- Modal intersection types, two-level languages, and staged synthesis
- Automatically splitting a two-stage lambda calculus
- Programming languages for interactive computing
- Reasoning about multi-stage programs
- Staged computation with staged lexical scope
- Label-free natural deduction systems for intuitionistic and classical modal logics
- Shifting the stage. Staging with delimited control
- Bilateral relevant logic
- The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
- On the semantics of intensionality
- Programs using syntax with first-class binders
- A temporal logic approach to binding-time analysis
- Embedding constructive K into intuitionistic K
- Language embeddings that preserve staging and safety
- The Logic of Proofs as a Foundation for Certifying Mobile Computation
- Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
- Specification patterns for reasoning about recursion through the store
- Justification logic as a foundation for certifying mobile computation
- scientific article; zbMATH DE number 1231474 (Why is no real title available?)
- Inlining as staged computation
- A note on harmony
- Capability-based localization of distributed and heterogeneous queries
- Bilateralism in proof-theoretic semantics
- A logic inspired by natural language: quantifiers as subnectors
- A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types
- Undecidability of QLTL and QCTL with two variables and one monadic predicate letter
- A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4
- Dual-context calculi for modal logic
- On harmony and permuting conversions
- General-elimination harmony and higher-level rules
- Modal dependent type theory and dependent right adjoints
- Axiomatic and dual systems for constructive necessity, a formally verified equivalence
- On the notion of canonical derivations from open assumptions and its role in proof-theoretic semantics
- General-elimination stability
- A polymorphic modal type system for Lisp-like multi-staged languages
- Realist consequence, epistemic inference, computational correctness
- Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism
- Staged computation with names and necessity
- A dual-context sequent calculus for the constructive modal logic S4
- A Logical Foundation for Environment Classifiers
- Primitive recursion for higher-order abstract syntax
- Exploring the Jungle of Intuitionistic Temporal Logics
- Normalization by evaluation for modal dependent type theory
- Realising intensional S4 and GL modalities
- \textsc{Synbit}: synthesizing bidirectional programs using unidirectional sketches
- Principles of staged static+dynamic partial analysis
- UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC
- Contextual modal type theory with polymorphic contexts
- A dependently typed multi-stage calculus
- Ill-founded proof systems for intuitionistic linear-time temporal logic
- Canonicity of proofs in constructive modal logic
- Towards logical foundations for probabilistic computation
- Curry and Howard meet Borel
- A subexponential view of domains in session types
- A categorical normalization proof for the modal lambda-calculus
- A modal analysis of metaprogramming, revisited (invited talk)
- Intuitionistic -calculus with the Lewis arrow
- Intuitionistic \textsf{S4} as a logic of topological spaces
- Polytime embedding of intuitionistic modal logics into their one-variable fragments
- Simple sequent systems for the modal logics K, D, T, and S4
- Minimal modal logics, constructive modal logics and their relations
- Multi-level contextual type theory
- Primitive recursive dependent type theory
- Handling mobility failures by modal types
- Unified sequent calculi and natural deduction systems for until-free linear-time temporal logics
- Sequent calculi and decidability for intuitionistic hybrid logic
- Cut-free Gentzen calculus for multimodal CK
- Constructive linear-time temporal logic: proof systems and Kripke semantics
This page was built for publication: A modal analysis of staged computation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3196622)
