Pages that link to "Item:Q1589654"

The following pages link to \(\pi\)-calculus in (Co)inductive-type theory (Q1589654):

Displaying 41 items.

• ASP\(_{\text{fun}}\) : a typed functional active object calculus (Q433340) (← links)
• Two case studies of semantics execution in Maude: CCS and LOTOS (Q816216) (← links)
• Mechanizing type environments in weak HOAS (Q897934) (← links)
• An exact correspondence between a typed pi-calculus and polarised proof-nets (Q974114) (← links)
• An interpretation of typed objects into typed \(\pi\)-calculus (Q1271311) (← links)
• On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions (Q1854404) (← links)
• \(\mathrm{HO}\pi\) in Coq (Q2031410) (← links)
• \( \pi\) with leftovers: a mechanisation in Agda (Q2117018) (← links)
• Mechanized metatheory revisited (Q2323447) (← links)
• Executable structural operational semantics in Maude (Q2369036) (← links)
• Fresh logic: Proof-theory and semantics for FM and nominal techniques (Q2372191) (← links)
• Structured coalgebras and minimal HD-automata for the \(\pi\)-calculus (Q2566037) (← links)
• Genericity and the \(\pi\)-calculus (Q2576663) (← links)
• Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts (Q2642466) (← links)
• Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda (Q2683037) (← links)
• A first-order syntax for the \(\pi\)-calculus in Isabelle/HOL using permutations (Q2841231) (← links)
• Developing (meta)theory of \(\lambda\)-calculus in the theory of contexts (Q2841233) (← links)
• Encoding generic judgments: preliminary results (Q2841234) (← links)
• The theory of contexts for first order and higher order abstract syntax (Q2841274) (← links)
• Comparing higher-order encodings in logical frameworks and tile logic (Q2841275) (← links)
• A framework for defining logical frameworks (Q2864157) (← links)
• A completeness proof for bisimulation in the pi-calculus using Isabelle (Q2871830) (← links)
• A Coq library for verification of concurrent programs (Q2871836) (← links)
• Specifying properties of concurrent computations in CLF (Q2871839) (← links)
• HOCore in Coq (Q2945640) (← links)
• The representational adequacy of <scp>Hybrid</scp> (Q3008233) (← links)
• Variable Binding, Symmetric Monoidal Closed Theories, and Bigraphs (Q3184683) (← links)
• Implementing Spi Calculus Using Nominal Techniques (Q3507444) (← links)
• (Q4365103) (← links)
• (Q4417854) (← links)
• (Q4484504) (← links)
• (Q4499314) (← links)
• (Q4536393) (← links)
• Proof-relevant π-calculus: a constructive account of concurrency and causality (Q4691184) (← links)
• Plugging-in proof development environments using<i>Locks</i>in<tt>LF</tt> (Q4691186) (← links)
• (Q5089301) (← links)
• A case study in programming coinductive proofs: Howe’s method (Q5236557) (← links)
• A Proof Theoretic Approach to Operational Semantics (Q5262970) (← links)
• An extensible approach to session polymorphism (Q5741569) (← links)
• Psi-calculi in Isabelle (Q5890661) (← links)
• Psi-calculi in Isabelle (Q5895110) (← links)