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

Publikation: Artikel i tidsskrift og konference artikel i tidsskrift › Konferenceartikel › Forskning › 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 .

Originalsprog	Engelsk
Bogserie	Lecture Notes in Computer Science
Sider (fra-til)	320-326
ISSN	0302-9743
DOI	https://doi.org/10.1007/978-3-540-71070-7_28
Status	Udgivet - 2008
Begivenhed	International Joint Conference, IJCAR 2008 - Sydney, Australien Varighed: 12 aug. 2008 → 15 aug. 2008 Konferencens nummer: 4

Konference

Konference	International Joint Conference, IJCAR 2008
Nummer	4
Land/Område	Australien
By	Sydney
Periode	12/08/2008 → 15/08/2008

Emneord

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

Adgang til dokumentet

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

Citationsformater

@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 -