MiniML

swMATH29625MaRDI QIDQ41339FDOQ41339

Author name not available (Why is that?)

Cited In (53)

• Specification patterns for reasoning about recursion through the store
• Program Logics for Homogeneous Generative Run-Time Meta-Programming
• On the Semantics of Intensionality
• Dual and axiomatic systems for constructive S4, a formally verified equivalence
• Axiomatic and dual systems for constructive necessity, a formally verified equivalence
• A dual-context sequent calculus for the constructive modal logic S4
• Intensional computation with higher-order functions
• A note on harmony
• Title not available (Why is that?)
• Intuitionistic hypothetical logic of proofs
• Title not available (Why is that?)
• Embedding Constructive K into Intuitionistic K
• Justification logic as a foundation for certifying mobile computation
• Fibrational modal type theory
• Subatomic natural deduction for a naturalistic first-order language with non-primitive identity
• Programs Using Syntax with First-Class Binders
• MetaML and multi-stage programming with explicit annotations
• Self-quotation in a typed, intensional lambda-calculus
• Connectionist computations of intuitionistic reasoning
• Incorporating quotation and evaluation into Church's type theory
• Classical natural deduction for S4 modal logic
• Primitive recursion for higher-order abstract syntax
• A general method for proving decidability of intuitionistic modal logics
• Nested sequents for intuitionistic modal logics via structural refinement
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• Harmony in multiple-conclusion natural-deduction
• Hypothetical logic of proofs
• Automatically Splitting a Two-Stage Lambda Calculus
• Type-specialized staged programming with process separation
• A Logical Foundation for Environment Classifiers
• Domain-free \(\lambda\mu\)-calculus
• Constructive linear-time temporal logic: proof systems and Kripke semantics
• Cut-free Gentzen calculus for multimodal CK
• Sequent calculi and decidability for intuitionistic hybrid logic
• Pattern matching as cut elimination
• Bilateralism in proof-theoretic semantics
• A logic inspired by natural language: quantifiers as subnectors
• The Logic of Proofs as a Foundation for Certifying Mobile Computation
• Game semantics for constructive modal logic
• Propositional primal logic with disjunction
• A proof-theoretic investigation of a logic of positions
• A modal analysis of staged computation
• Modal dependent type theory and dependent right adjoints
• Strong normalization in some temporal substructural logics
• A framework for intuitionistic grammar logics
• Capability-based localization of distributed and heterogeneous queries
• General-Elimination Harmony and Higher-Level Rules
• Encoding types in ML-like languages
• A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types
• Programming languages for interactive computing
• On harmony and permuting conversions
• General-elimination stability
• Undecidability of QLTL and QCTL with two variables and one monadic predicate letter

This page was built for software: MiniML