A modal analysis of staged computation
From MaRDI portal
Publication:3196622
DOI10.1145/382780.382785zbMath1323.68107OpenAlexW2029408547WikidataQ56211000 ScholiaQ56211000MaRDI QIDQ3196622
Publication date: 30 October 2015
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/382780.382785
Modal logic (including the logic of norms) (03B45) Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40)
Related Items
Intuitionistic hypothetical logic of proofs, A dual-context sequent calculus for the constructive modal logic S4, Self-quotation in a typed, intensional lambda-calculus, Pattern matching as cut elimination, Label-free natural deduction systems for intuitionistic and classical modal logics, Nested sequents for intuitionistic modal logics via structural refinement, Game semantics for constructive modal logic, 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, Shifting the stage, Embedding Constructive K into Intuitionistic K, Capability-based localization of distributed and heterogeneous queries, BILATERAL RELEVANT LOGIC, Type-specialized staged programming with process separation, Specification patterns for reasoning about recursion through the store, Realist Consequence, Epistemic Inference, Computational Correctness, Exploring the Jungle of Intuitionistic Temporal Logics, Normalization by evaluation for modal dependent type theory, Justification logic as a foundation for certifying mobile computation, \textsc{Synbit}: synthesizing bidirectional programs using unidirectional sketches, UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC, Semantical analysis of contextual types, A proof-theoretic investigation of a logic of positions, A framework for intuitionistic grammar logics, The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types, A note on harmony, Dual and axiomatic systems for constructive S4, a formally verified equivalence, On the Semantics of Intensionality, Programs Using Syntax with First-Class Binders, Bilateralism in proof-theoretic semantics, A logic inspired by natural language: quantifiers as subnectors, Intensional computation with higher-order functions, Domain-Freeλµ-Calculus, Fibrational modal type theory, On harmony and permuting conversions, Incorporating quotation and evaluation into Church's type theory, General-elimination stability, Classical natural deduction for S4 modal logic, Hypothetical logic of proofs, Harmony in multiple-conclusion natural-deduction, Subatomic natural deduction for a naturalistic first-order language with non-primitive identity, Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism, Connectionist computations of intuitionistic reasoning, The Logic of Proofs as a Foundation for Certifying Mobile Computation, A general method for proving decidability of intuitionistic modal logics, Primitive recursion for higher-order abstract syntax, Automatically Splitting a Two-Stage Lambda Calculus, General-Elimination Harmony and Higher-Level Rules, Unnamed Item, Modal dependent type theory and dependent right adjoints, A Logical Foundation for Environment Classifiers, A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4, Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages, Axiomatic and dual systems for constructive necessity, a formally verified equivalence, 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, Encoding types in ML-like languages, MetaML and multi-stage programming with explicit annotations, ON THE NOTION OF CANONICAL DERIVATIONS FROM OPEN ASSUMPTIONS AND ITS ROLE IN PROOF-THEORETIC SEMANTICS, Programming Languages For Interactive Computing
Uses Software
