The following pages link to Types for Proofs and Programs (Q5712317):
Displaying 45 items.
- Dynamic spaces in concurrent constraint programming (Q281160) (← links)
- Existential type systems between Church and Curry style (type-free style) (Q402117) (← links)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- Relating state-based and process-based concurrency through linear logic (full-version) (Q731895) (← links)
- Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types (Q880987) (← links)
- A logical characterization of forward and backward chaining in the inverse method (Q928660) (← links)
- Canonical HybridLF: extending Hybrid with dependent types (Q1744412) (← links)
- Logical approximation for program analysis (Q1929363) (← links)
- \(\mathrm{HO}\pi\) in Coq (Q2031410) (← links)
- Subformula linking for intuitionistic logic with application to type theory (Q2055855) (← links)
- Coherence via focusing for symmetric skew monoidal categories (Q2148789) (← links)
- Kleene star, subexponentials without contraction, and infinite computations (Q2234420) (← links)
- Formalizing adequacy: a case study for higher-order abstract syntax (Q2392483) (← links)
- SMT proof checking using a logical framework (Q2441776) (← links)
- On the unity of duality (Q2482843) (← links)
- A proof theoretic view of spatial and temporal dependencies in biochemical systems (Q2628774) (← links)
- Explicit contexts in LF (extended abstract) (Q2804940) (← links)
- Case analysis of higher-order data (Q2804942) (← links)
- Hybridizing a logical framework (Q2867954) (← links)
- Normalization for the simply-typed lambda-calculus in Twelf (Q2871835) (← links)
- A Coq library for verification of concurrent programs (Q2871836) (← links)
- Specifying properties of concurrent computations in CLF (Q2871839) (← links)
- Redundancy elimination for LF (Q2871840) (← links)
- Induction on concurrent terms (Q2871870) (← links)
- Structural Focalization (Q2946730) (← links)
- LINCX: A Linear Logical Framework with First-Class Contexts (Q2988658) (← links)
- Higher-Order Dynamic Pattern Unification for Dependent Types and Records (Q3007654) (← links)
- Implementing Cantor’s Paradise (Q3179294) (← links)
- I Got Plenty o’ Nuttin’ (Q3188289) (← links)
- (Q3384910) (← links)
- Syntactic Metatheory of Higher-Order Subtyping (Q3540196) (← links)
- Celf – A Logical Framework for Deductive and Concurrent Systems (System Description) (Q3541713) (← links)
- Coordination: Reo, Nets, and Logic (Q3603000) (← links)
- Refinement Types as Proof Irrelevance (Q3637193) (← links)
- Expressing additives using multiplicatives and subexponentials (Q4637626) (← links)
- Relating State-Based and Process-Based Concurrency through Linear Logic (Q4917995) (← links)
- (Q4957789) (← links)
- (Q5018483) (← links)
- ANF preserves dependent types up to extensional equality (Q5051989) (← links)
- Back to futures (Q5063251) (← links)
- POPLMark reloaded: Mechanizing proofs by logical relations (Q5110924) (← links)
- A fibrational framework for substructural and modal logics (Q5111322) (← links)
- Finitary type theories with and without contexts (Q6053849) (← links)
- Towards substructural property-based testing (Q6102253) (← links)
- Normalization for multimodal type theory (Q6649430) (← links)
