Celf – A Logical Framework for Deductive and Concurrent Systems (System Description)

Anders Schack-Nielsen; Carsten Schürmann

doi:10.1007/978-3-540-71070-7_28

Celf – A Logical Framework for Deductive and Concurrent Systems (System Description)

Anders Schack-Nielsen, Carsten Schürmann

Computer Science

Research output: Journal Article or Conference Article in Journal › Conference article › Research › peer-review

Abstract

CLF (Concurrent LF) [CPWW02a] is a logical framework for specifying and implementing deductive and concurrent systems from areas, such as programming language theory, security protocol analysis, process algebras, and logics. Celf is an implementation of the CLF type theory that extends the LF type theory by linear types to support representation of state and a monad to support representation of concurrency. It relies on the judgments-as-types methodology for specification and the interpretation of CLF signatures as concurrent logic programs [LPPW05] for experimentation. Celf is written in Standard ML and compiles with MLton, MLKit, and SML/NJ. The source code and a collection of examples are available from http://www.twelf.org/~celf .

Original language	English
Book series	Lecture Notes in Computer Science
Pages (from-to)	320-326
ISSN	0302-9743
DOIs	https://doi.org/10.1007/978-3-540-71070-7_28
Publication status	Published - 2008
Event	International Joint Conference, IJCAR 2008 - Sydney, Australia Duration: 12 Aug 2008 → 15 Aug 2008 Conference number: 4

Conference

Conference	International Joint Conference, IJCAR 2008
Number	4
Country/Territory	Australia
City	Sydney
Period	12/08/2008 → 15/08/2008

Keywords

Concurrent Logical Framework
Celf
Linear Types
Concurrency
Judgments-as-Types

Access to Document

10.1007/978-3-540-71070-7_28

Cite this

@inproceedings{e6a3f9b0e2ef11dda259000ea68e967b,

title = "Celf – A Logical Framework for Deductive and Concurrent Systems (System Description)",

abstract = "CLF (Concurrent LF) [CPWW02a] is a logical framework for specifying and implementing deductive and concurrent systems from areas, such as programming language theory, security protocol analysis, process algebras, and logics. Celf is an implementation of the CLF type theory that extends the LF type theory by linear types to support representation of state and a monad to support representation of concurrency. It relies on the judgments-as-types methodology for specification and the interpretation of CLF signatures as concurrent logic programs [LPPW05] for experimentation. Celf is written in Standard ML and compiles with MLton, MLKit, and SML/NJ. The source code and a collection of examples are available from http://www.twelf.org/~celf .",

keywords = "Concurrent Logical Framework, Celf, Linear Types, Concurrency, Judgments-as-Types, Concurrent Logical Framework, Celf, Linear Types, Concurrency, Judgments-as-Types",

author = "Anders Schack-Nielsen and Carsten Sch{\"u}rmann",

note = "Serie: Lecture Notes in Computer Science, Springer, 5195/2008, 0302-9743, 1611-3349 Volumne: 5195/2008; International Joint Conference, IJCAR 2008 ; Conference date: 12-08-2008 Through 15-08-2008",

year = "2008",

doi = "10.1007/978-3-540-71070-7_28",

language = "English",

pages = "320--326",

journal = "Lecture Notes in Computer Science",

issn = "0302-9743",

publisher = "Springer",

}

TY - GEN

T1 - Celf – A Logical Framework for Deductive and Concurrent Systems (System Description)

AU - Schack-Nielsen, Anders

AU - Schürmann, Carsten

N1 - Conference code: 4

PY - 2008

Y1 - 2008

N2 - CLF (Concurrent LF) [CPWW02a] is a logical framework for specifying and implementing deductive and concurrent systems from areas, such as programming language theory, security protocol analysis, process algebras, and logics. Celf is an implementation of the CLF type theory that extends the LF type theory by linear types to support representation of state and a monad to support representation of concurrency. It relies on the judgments-as-types methodology for specification and the interpretation of CLF signatures as concurrent logic programs [LPPW05] for experimentation. Celf is written in Standard ML and compiles with MLton, MLKit, and SML/NJ. The source code and a collection of examples are available from http://www.twelf.org/~celf .

AB - CLF (Concurrent LF) [CPWW02a] is a logical framework for specifying and implementing deductive and concurrent systems from areas, such as programming language theory, security protocol analysis, process algebras, and logics. Celf is an implementation of the CLF type theory that extends the LF type theory by linear types to support representation of state and a monad to support representation of concurrency. It relies on the judgments-as-types methodology for specification and the interpretation of CLF signatures as concurrent logic programs [LPPW05] for experimentation. Celf is written in Standard ML and compiles with MLton, MLKit, and SML/NJ. The source code and a collection of examples are available from http://www.twelf.org/~celf .

KW - Concurrent Logical Framework

KW - Celf

KW - Linear Types

KW - Concurrency

KW - Judgments-as-Types

KW - Concurrent Logical Framework

KW - Celf

KW - Linear Types

KW - Concurrency

KW - Judgments-as-Types

U2 - 10.1007/978-3-540-71070-7_28

DO - 10.1007/978-3-540-71070-7_28

M3 - Conference article

SN - 0302-9743

SP - 320

EP - 326

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

T2 - International Joint Conference, IJCAR 2008

Y2 - 12 August 2008 through 15 August 2008

ER -