LINCX: A Linear Logical Framework with First-Class Contexts

DOI10.1007/978-3-662-54434-1_20zbMath1485.68065OpenAlexW2595518539MaRDI QIDQ2988658

Agata Murawska, Brigitte Pientka, Shawn Otis, Aina Linn Georges

Publication date: 19 May 2017

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-54434-1_20

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Towards substructural property-based testing ⋮ \( \pi\) with leftovers: a mechanisation in Agda

Uses Software

• Coq
• Beluga
• Twelf
• Lincx
• Charge!

Cites Work

• Unnamed Item
• Linear continuation-passing
• A two-level logic approach to reasoning about computations
• A Meta Linear Logical Framework
• Charge!
• Programming Type-Safe Transformations Using Higher-Order Abstract Syntax
• Programming with binders and indexed data-types
• Indexed codata types
• Practical Tactics for Separation Logic
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• Inductive Beluga: Programming Proofs
• A Contextual Logical Framework
• Session Types as Intuitionistic Linear Propositions
• A framework for defining logics
• Representing Control: a Study of the CPS Transformation
• A Linear Spine Calculus
• On regions and linear types (extended abstract)
• Contextual modal type theory
• Types for Proofs and Programs
• Reasoning with higher-order abstract syntax in a logical framework
• Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• Programming Languages and Systems

This page was built for publication: LINCX: A Linear Logical Framework with First-Class Contexts