Types for Proofs and Programs
From MaRDI portal
Publication:5712317
DOI10.1007/b98246zbMath1100.68548OpenAlexW4298423642MaRDI QIDQ5712317
No author found.
Publication date: 23 December 2005
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/b98246
Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (44)
Dynamic spaces in concurrent constraint programming ⋮ A proof theoretic view of spatial and temporal dependencies in biochemical systems ⋮ ANF preserves dependent types up to extensional equality ⋮ Implementing Cantor’s Paradise ⋮ Coherence via focusing for symmetric skew monoidal categories ⋮ Back to futures ⋮ Unnamed Item ⋮ I Got Plenty o’ Nuttin’ ⋮ Formalizing adequacy: a case study for higher-order abstract syntax ⋮ Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types ⋮ Structural Focalization ⋮ Logical approximation for program analysis ⋮ Finitary type theories with and without contexts ⋮ Existential type systems between Church and Curry style (type-free style) ⋮ A logical framework with higher-order rational (circular) terms ⋮ Towards substructural property-based testing ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ Unnamed Item ⋮ Unnamed Item ⋮ SMT proof checking using a logical framework ⋮ LINCX: A Linear Logical Framework with First-Class Contexts ⋮ Syntactic Metatheory of Higher-Order Subtyping ⋮ A logical characterization of forward and backward chaining in the inverse method ⋮ Celf – A Logical Framework for Deductive and Concurrent Systems (System Description) ⋮ Expressing additives using multiplicatives and subexponentials ⋮ Kleene star, subexponentials without contraction, and infinite computations ⋮ Higher-Order Dynamic Pattern Unification for Dependent Types and Records ⋮ Canonical HybridLF: extending Hybrid with dependent types ⋮ Relating State-Based and Process-Based Concurrency through Linear Logic ⋮ On the unity of duality ⋮ Coordination: Reo, Nets, and Logic ⋮ \(\mathrm{HO}\pi\) in Coq ⋮ Relating state-based and process-based concurrency through linear logic (full-version) ⋮ Explicit Contexts in LF (Extended Abstract) ⋮ Case Analysis of Higher-Order Data ⋮ Unnamed Item ⋮ Subformula linking for intuitionistic logic with application to type theory ⋮ Refinement Types as Proof Irrelevance ⋮ 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
Uses Software
This page was built for publication: Types for Proofs and Programs
