A concurrent logical framework: The propositional fragment
From MaRDI portal
Recommendations
Cited in
(51)- Canonical HybridLF: extending Hybrid with dependent types
- Logical approximation for program analysis
- \(\mathrm{HO}\pi\) in Coq
- Subformula linking for intuitionistic logic with application to type theory
- Coherence via focusing for symmetric skew monoidal categories
- Kleene star, subexponentials without contraction, and infinite computations
- Formalizing adequacy: a case study for higher-order abstract syntax
- SMT proof checking using a logical framework
- On the unity of duality
- A proof theoretic view of spatial and temporal dependencies in biochemical systems
- Explicit contexts in LF (extended abstract)
- Case analysis of higher-order data
- Dynamic spaces in concurrent constraint programming
- Hybridizing a logical framework
- Normalization for the simply-typed lambda-calculus in Twelf
- A Coq library for verification of concurrent programs
- Specifying properties of concurrent computations in CLF
- Redundancy elimination for LF
- Induction on concurrent terms
- Structural focalization
- \textsc{Lincx}: a linear logical framework with first-class contexts
- Higher-order dynamic pattern unification for dependent types and records
- Implementing Cantor's paradise
- I got plenty o' nuttin'
- Everybody's got to be somewhere
- Syntactic Metatheory of Higher-Order Subtyping
- Celf – A Logical Framework for Deductive and Concurrent Systems (System Description)
- Coordination: Reo, Nets, and Logic
- Refinement Types as Proof Irrelevance
- Existential type systems between Church and Curry style (type-free style)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Expressing additives using multiplicatives and subexponentials
- Relating state-based and process-based concurrency through linear logic
- Hereditary substitution for the \(\lambda \Delta \)-calculus
- Towards meta-reasoning in the concurrent logical framework CLF
- Formalization of automated trading systems in a concurrent linear framework
- ANF preserves dependent types up to extensional equality
- Back to futures
- POPLMark reloaded: mechanizing proofs by logical relations
- scientific article; zbMATH DE number 7204444 (Why is no real title available?)
- Finitary type theories with and without contexts
- A logical framework with higher-order rational (circular) terms
- Towards substructural property-based testing
- Normalization for multimodal type theory
- Normalization for multimodal type theory
- Coherence via focusing for symmetric skew monoidal and symmetric skew closed categories
- Deductive systems and coherence for skew prounital closed categories
- Linear logic using negative connectives
- Relating state-based and process-based concurrency through linear logic (full-version)
- Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types
- A logical characterization of forward and backward chaining in the inverse method
This page was built for publication: A concurrent logical framework: The propositional fragment
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5712317)
