# Towards Meta-Reasoning in the Concurrent Logical Framework CLF

@inproceedings{Cervesato2013TowardsMI, title={Towards Meta-Reasoning in the Concurrent Logical Framework CLF}, author={Iliano Cervesato and Jorge Luis Sacchini}, booktitle={EXPRESS/SOS}, year={2013} }

The concurrent logical framework CLF is an extension of the logical framework LF designed to specify concurrent and distributed languages. While it can be used to define a variety of formalisms, reasoning about such languages within CLF has proved elusive. In this paper, we propose an extension of LF that allows us to express properties of CLF specifications. We illustrate the approach with a proof of safety for a small language with a parallel semantics.

#### Figures and Topics from this paper

#### 3 Citations

Formalization of Automated Trading Systems in a Concurrent Linear Framework

- Computer Science
- Linearity-TLLA@FLoC
- 2018

A declarative and modular specification of an automated trading system (ATS) in the concurrent linear framework CLF is presented and the verification of two representative properties of trading systems using generative grammars is outlined. Expand

Collected Abstracts of the 2013 LIX Colloquium on the Theory and Application of Formal Proofs November

- 2013

In this talk, we present a new syntax for Linear Logic, inspired by natural deduction. In the sequent-calculus formulation of this syntax, the leaves of sequent trees can be labelled not only with… Expand

Proof Composition Mechanisms and Their Geometric Interpretation

- 2013

#### References

SHOWING 1-10 OF 33 REFERENCES

Specifying Properties of Concurrent Computations in CLF

- Computer Science, Mathematics
- Electron. Notes Theor. Comput. Sci.
- 2008

The representation techniques available within CLF are illustrated by applying them to an asynchronous pi-calculus with correspondence assertions, including its dynamic semantics, safety criterion, and a type system with latent effects due to Gordon and Jeffrey. Expand

Trace matching in a concurrent logical framework

- Mathematics
- LFMTP '12
- 2012

Matching and unification play an important role in implementations of proof assistants, logical frameworks, and logic programming languages. In particular, matching is at the heart of many reasoning… Expand

A Concurrent Logical Framework: The Propositional Fragment

- Computer Science
- TYPES
- 2003

The propositional fragment CLF0 of the Concurrent Logical Framework (CLF) is presented, which is a novel combination of lax logic and dual intuitionistic linear logic that allows the natural representation of concurrent computations in an object language. Expand

A Concurrent Logical Framework II: Examples and Applications

- Computer Science
- 2003

This report illustrates the expressive power of the CLF framework by encoding several different concurrent languages including both the synchronous and asynchronous pi-calculus, an ML-like language with futures, lazy evaluation and concurrency primitives in the style of CML, Petri nets and finally, the security protocol specification language MSR. Expand

A concurrent logical framework I: Judgments and properties

- Mathematics
- 2003

Abstract : The Concurrent Logical Framework, or CLF, is a new logical framework in which concurrent computations can be represented as monadic objects, for which there is an intrinsic notion of… Expand

A Linear Logical Framework

- Computer Science
- Inf. Comput.
- 2002

The linear type theory LLF is presented as the formal basis for a conservative extension of the LF logical framework and can be given an operational interpretation as a logic programming language under which the representations above can be used for type inference, evaluation and cut-elimination. Expand

Implementing Substructural Logical Frameworks

- Computer Science
- 2011

This thesis develops the theoretical infrastructure required to implement — and gives an implementation of — a new logical framework that extends LF with the concepts of both linear resources and affine resources, and proves strong normalization, type preservation, and confluence for a context-split-oblivious reduction semantics. Expand

Substructural logical specifications

- Computer Science
- 2012

This dissertation introduces and demonstrates four methodologies for developing and using substructural logical frameworks for specifying and reasoning about stateful and concurrent systems, and shows that generative invariants can form the basis of progress-and-preservation-style reasoning about programming languages encoded in SLS. Expand

System Description: Twelf - A Meta-Logical Framework for Deductive Systems

- Computer Science
- CADE
- 1999

Twelf is a meta-logical framework for the specification, implementation, and meta-theory of deductive systems from the theory of programming languages and logics and is a significant extension and complete reimplementation of the Elf system. Expand

Substructural Operational Semantics and Linear Destination-Passing Style (Invited Talk)

- Computer Science
- APLAS
- 2004

Substructural operational semantics (SSOS), a presentation form for the semantics of programming languages, combines ideas from structural operational semantics and type theories based on substructural logics in order to obtain a rich, uniform, and modular framework. Expand