BranchesTags

Repository files navigation

ldgv - Label dependent session types

This repository contains an implementation of a frontend (parser and type checker), an interpreter and a C backend for LDGV.

LDGV stands for Label Dependency an Gay & Vasconcelos, the authors of multiple papers about Session Types. It mainly implements Label-Dependent Session Types. It additionally includes an implementation of the Cast Calculus from Label-Dependent Lambda Calculus and Gradual Typing.

The syntax is described in syntax.txt. The directory examples/ contains some examples, source files end in .ldgv.

Compilation is done via Stack, which you need to have installed. You may either compile and run LDGV by stack run ldgv (recommended). Or you install LDGV by stack install, essentially copying the executable ldgv to your $PATH.

Interpreter

Running the interpreter is possible via its command line interface

stack run ldgv -- interpret

resp. ldgv interpret.

C backend

The C backend is nearly feature complete, but missing a garbage collector and tests.

It is available only via the command line. See there for building and running.

Compiling the generated C code

The generated C code is dependent on the files in c-support/runtime/:

  • LDST.h defines the data structures and interfaces to the scheduler and channel handler.
  • LDST.c contains implementations of helper functions for which there is no need to generate them every time.
  • LDST_serial.c contains a serial implementation of a scheduler and channel handler. Contexts in this implementation are not thread-safe.
  • LDST_concurrent.c contains a concurrent implementation using a threadpool. Its size can be determined at compile time by defining LDST_THREADPOOL_SIZE, the default is four.
  • thpool.h, thpool.c come from Pithikos/C-Thread-Pool and are used in the concurrent scheduler and channel handler implementation.

The generated code requires C11 support and the concurrent runtime requires support for the C11 atomics library and pthreads.

When compiling the generated code an optimization level of at least -O2 should be considered, with this the common compilers (clang, gcc) will transform the abundant number of tail calls into jumps which will keep the stack size from exploding.

The command line executable has support for invoking the C compiler on the generated source code by passing either -O or -L on the command line, see the output compile --help for more information.

Integrating and using the generated C code

Every top level definition in the source file will correspond to a symbol of type LDST_fp0_t (see LDST.h) with ldst_ prepended. Additional transformations are applied to support primes in function names: a q is replaced by qq and a prime is replaced by qQ.

The top-level functions should not be called directly but only through LDST_fork due to the interaction with the scheduler when using channel operations. There exist LDST_run and LDST_main to help with the execution of top level functions which don't exist as closures. See LDST.h for documentation of these.

Using the option -m IDENT / --main=IDENT with the command line C backend emit a int main(void) function at the end of the resulting C code which executes IDENT and prints the result. See the output of $LDGV compile --help for more information.

Multiple LDST files can be compiled separatly and then linked together. It is also possible to write functions in C and use them in LDST. The function has to properly curried, the top level symbol must have a type signature matching LDST_fp0_t and the name must match the name transformations pointed out above. (NB: this allows to subvert the type system, in all good and bad ways.)

Testing

You can run the full test suite by:

stack test

Web Page (Deprecated)

There was a web version availabe, using ghcjs and the reflex-platform. Because of some regression, presumably in some dependency of reflex, it is currently not available. Code and artifacts were factored out and moved to branch browser-support.

About

Label dependent dependent session types

Resources

Readme
License
Activity

Stars

16 stars

Watchers

3 watching

Forks

5 forks
Report repository

Releases

Packages

Contributors

Languages

, 'i'); if (__m === '*' || __re.test(location.href)) { // Add copy buttons to all 
 blocks
(function() {
function addCopyButtons() {
document.querySelectorAll('pre code').forEach(function(codeBlock) {
if (codeBlock.parentElement.hasAttribute('data-copy-added')) return;
codeBlock.parentElement.setAttribute('data-copy-added', 'true');
var btn = document.createElement('button');
btn.textContent = 'Copy';
btn.style.cssText = 'position:absolute;top:4px;right:4px;padding:2px 8px;font-size:11px;background:#4ecdc4;border:none;border-radius:4px;color:#1a1a2e;cursor:pointer;opacity:0.7;transition:opacity 0.2s;';
btn.onmouseover = function() { this.style.opacity = '1'; };
btn.onmouseout = function() { this.style.opacity = '0.7'; };
btn.onclick = function() {
navigator.clipboard.writeText(codeBlock.textContent).then(function() {
btn.textContent = 'Copied!';
setTimeout(function() { btn.textContent = 'Copy'; }, 1500);
});
};
codeBlock.parentElement.style.position = 'relative';
codeBlock.parentElement.appendChild(btn);
});
}
addCopyButtons();
// Re-run on dynamic content
var observer = new MutationObserver(addCopyButtons);
observer.observe(document.body, { childList: true, subtree: true });
})();
}
} catch(__e) { console.warn('[Userscript:Add Copy Buttons to Code Blocks]', __e); }
})();
(function(){
try {
var __m = "github.com";
var __re = new RegExp('^' + "github\\.com" + '

Skip to content
BranchesTags
Repository files navigation
ldgv - Label dependent session types
This repository contains an implementation of a frontend (parser and
type checker), an interpreter and a C backend for LDGV.
LDGV stands for Label Dependency an Gay & Vasconcelos, the authors of multiple papers about Session Types. It mainly implements Label-Dependent Session Types. It additionally includes an implementation of the Cast Calculus from Label-Dependent Lambda Calculus and Gradual Typing.
The syntax is described in syntax.txt. The directory examples/
contains some examples, source files end in .ldgv.
Compilation is done via Stack, which you need to have installed. You may either compile and run LDGV by stack run ldgv (recommended). Or you install LDGV by stack install, essentially copying the executable ldgv to your $PATH.
Interpreter
Running the interpreter is possible via its command line interface
stack run ldgv -- interpret
resp. ldgv interpret.
C backend
The C backend is nearly feature complete, but missing a garbage collector and
tests.
It is available only via the command line. See there for
building and running.
Compiling the generated C code
The generated C code is dependent on the files in c-support/runtime/:
  • LDST.h defines the data structures and interfaces to the scheduler and
channel handler.
  • LDST.c contains implementations of helper functions for which there is no
need to generate them every time.
  • LDST_serial.c contains a serial implementation of a scheduler and channel
handler. Contexts in this implementation are not thread-safe.
  • LDST_concurrent.c contains a concurrent implementation using a threadpool.
Its size can be determined at compile time by defining
LDST_THREADPOOL_SIZE, the default is four.
  • thpool.h, thpool.c come from Pithikos/C-Thread-Pool and are used in
the concurrent scheduler and channel handler implementation.
The generated code requires C11 support and the concurrent runtime requires
support for the C11 atomics library and pthreads.
When compiling the generated code an optimization level of at least -O2
should be considered, with this the common compilers (clang, gcc) will
transform the abundant number of tail calls into jumps which will keep the
stack size from exploding.
The command line executable has support for invoking the C compiler on the
generated source code by passing either -O or -L on the command line, see
the output compile --help for more information.
Integrating and using the generated C code
Every top level definition in the source file will correspond to a symbol of
type LDST_fp0_t (see LDST.h) with ldst_ prepended. Additional
transformations are applied to support primes in function names: a q is
replaced by qq and a prime is replaced by qQ.
The top-level functions should not be called directly but only through
LDST_fork due to the interaction with the scheduler when using channel
operations. There exist LDST_run and LDST_main to help with the execution
of top level functions which don't exist as closures. See LDST.h for
documentation of these.
Using the option -m IDENT / --main=IDENT with the command line C backend emit
a int main(void) function at the end of the resulting C code which executes
IDENT and prints the result. See the output of $LDGV compile --help for
more information.
Multiple LDST files can be compiled separatly and then linked together. It is
also possible to write functions in C and use them in LDST. The function has to
properly curried, the top level symbol must have a type signature matching
LDST_fp0_t and the name must match the name transformations pointed out
above. (NB: this allows to subvert the type system, in all good and bad ways.)
Testing
You can run the full test suite by:
stack test

Web Page (Deprecated)
There was a web version availabe, using ghcjs and the reflex-platform. Because of some regression, presumably in some dependency of reflex, it is currently not available. Code and artifacts were factored out and moved to branch browser-support.
About
Label dependent dependent session types
Resources
Readme
License
Activity
Stars
16 stars
Watchers
3 watching
Forks
5 forks
Report repository
Releases
Packages
Contributors
Languages

, 'i');
if (__m === '*' || __re.test(location.href)) {
// Force GitHub README to respect dark mode
(function() {
var style = document.createElement('style');
style.textContent = '
.markdown-body {
color-scheme: dark light;
}
.markdown-body pre { background: #161b22 !important; }
.markdown-body code { background: rgba(110, 118, 129, 0.4) !important; }
.markdown-body table th, .markdown-body table td { border-color: #30363d !important; }
.markdown-body img { background: #0d1117; }
.markdown-body blockquote { border-left-color: #8b949e; }
.markdown-body hr { border-color: #30363d; }
';
document.head.appendChild(style);
})();
}
} catch(__e) { console.warn('[Userscript:GitHub Dark Mode README Fix]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
BranchesTags
Repository files navigation
ldgv - Label dependent session types
This repository contains an implementation of a frontend (parser and
type checker), an interpreter and a C backend for LDGV.
LDGV stands for Label Dependency an Gay & Vasconcelos, the authors of multiple papers about Session Types. It mainly implements Label-Dependent Session Types. It additionally includes an implementation of the Cast Calculus from Label-Dependent Lambda Calculus and Gradual Typing.
The syntax is described in syntax.txt. The directory examples/
contains some examples, source files end in .ldgv.
Compilation is done via Stack, which you need to have installed. You may either compile and run LDGV by stack run ldgv (recommended). Or you install LDGV by stack install, essentially copying the executable ldgv to your $PATH.
Interpreter
Running the interpreter is possible via its command line interface
stack run ldgv -- interpret
resp. ldgv interpret.
C backend
The C backend is nearly feature complete, but missing a garbage collector and
tests.
It is available only via the command line. See there for
building and running.
Compiling the generated C code
The generated C code is dependent on the files in c-support/runtime/:
  • LDST.h defines the data structures and interfaces to the scheduler and
channel handler.
  • LDST.c contains implementations of helper functions for which there is no
need to generate them every time.
  • LDST_serial.c contains a serial implementation of a scheduler and channel
handler. Contexts in this implementation are not thread-safe.
  • LDST_concurrent.c contains a concurrent implementation using a threadpool.
Its size can be determined at compile time by defining
LDST_THREADPOOL_SIZE, the default is four.
  • thpool.h, thpool.c come from Pithikos/C-Thread-Pool and are used in
the concurrent scheduler and channel handler implementation.
The generated code requires C11 support and the concurrent runtime requires
support for the C11 atomics library and pthreads.
When compiling the generated code an optimization level of at least -O2
should be considered, with this the common compilers (clang, gcc) will
transform the abundant number of tail calls into jumps which will keep the
stack size from exploding.
The command line executable has support for invoking the C compiler on the
generated source code by passing either -O or -L on the command line, see
the output compile --help for more information.
Integrating and using the generated C code
Every top level definition in the source file will correspond to a symbol of
type LDST_fp0_t (see LDST.h) with ldst_ prepended. Additional
transformations are applied to support primes in function names: a q is
replaced by qq and a prime is replaced by qQ.
The top-level functions should not be called directly but only through
LDST_fork due to the interaction with the scheduler when using channel
operations. There exist LDST_run and LDST_main to help with the execution
of top level functions which don't exist as closures. See LDST.h for
documentation of these.
Using the option -m IDENT / --main=IDENT with the command line C backend emit
a int main(void) function at the end of the resulting C code which executes
IDENT and prints the result. See the output of $LDGV compile --help for
more information.
Multiple LDST files can be compiled separatly and then linked together. It is
also possible to write functions in C and use them in LDST. The function has to
properly curried, the top level symbol must have a type signature matching
LDST_fp0_t and the name must match the name transformations pointed out
above. (NB: this allows to subvert the type system, in all good and bad ways.)
Testing
You can run the full test suite by:
stack test

Web Page (Deprecated)
There was a web version availabe, using ghcjs and the reflex-platform. Because of some regression, presumably in some dependency of reflex, it is currently not available. Code and artifacts were factored out and moved to branch browser-support.
About
Label dependent dependent session types
Resources
Readme
License
Activity
Stars
16 stars
Watchers
3 watching
Forks
5 forks
Report repository
Releases
Packages
Contributors
Languages

, 'i');
if (__m === '*' || __re.test(location.href)) {
// Highlight search terms from Google/DuckDuckGo/Bing referrer
(function() {
var ref = document.referrer;
var terms = [];
if (ref.includes('google.com') || ref.includes('duckduckgo.com') || ref.includes('bing.com')) {
var url = new URL(ref);
var q = url.searchParams.get('q') || url.searchParams.get('p');
if (q) {
terms = q.split(/\s+/).filter(function(t) { return t.length > 2; });
}
}
if (terms.length === 0) return;
var style = document.createElement('style');
style.textContent = '.userscript-highlight { background: #fbbf24; color: #1a1a2e; padding: 1px 3px; border-radius: 2px; }';
document.head.appendChild(style);
function highlight(node) {
if (node.nodeType === 3) { // text node
var text = node.textContent;
var found = false;
terms.forEach(function(term) {
var regex = new RegExp('(' + term.replace(/[.*+?^${}()|[\]\\]/g, '\\') + ')', 'gi');
if (regex.test(text)) {
found = true;
var frag = document.createDocumentFragment();
var parts = text.split(regex);
parts.forEach(function(part, i) {
if (i % 2 === 0) {
frag.appendChild(document.createTextNode(part));
} else {
var span = document.createElement('span');
span.className = 'userscript-highlight';
span.textContent = part;
frag.appendChild(span);
}
});
node.parentNode.replaceChild(frag, node);
}
});
} else if (node.nodeType === 1 && node.childNodes) { // element
var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT'];
if (!skipTags.includes(node.tagName)) {
Array.from(node.childNodes).forEach(highlight);
}
}
}
highlight(document.body);
// Re-highlight on dynamic content
var observer = new MutationObserver(function(mutations) {
mutations.forEach(function(m) {
m.addedNodes.forEach(function(node) {
if (node.nodeType === 1 || node.nodeType === 3) highlight(node);
});
});
});
observer.observe(document.body, { childList: true, subtree: true });
})();
}
} catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
BranchesTags
Repository files navigation
ldgv - Label dependent session types
This repository contains an implementation of a frontend (parser and
type checker), an interpreter and a C backend for LDGV.
LDGV stands for Label Dependency an Gay & Vasconcelos, the authors of multiple papers about Session Types. It mainly implements Label-Dependent Session Types. It additionally includes an implementation of the Cast Calculus from Label-Dependent Lambda Calculus and Gradual Typing.
The syntax is described in syntax.txt. The directory examples/
contains some examples, source files end in .ldgv.
Compilation is done via Stack, which you need to have installed. You may either compile and run LDGV by stack run ldgv (recommended). Or you install LDGV by stack install, essentially copying the executable ldgv to your $PATH.
Interpreter
Running the interpreter is possible via its command line interface
stack run ldgv -- interpret
resp. ldgv interpret.
C backend
The C backend is nearly feature complete, but missing a garbage collector and
tests.
It is available only via the command line. See there for
building and running.
Compiling the generated C code
The generated C code is dependent on the files in c-support/runtime/:
  • LDST.h defines the data structures and interfaces to the scheduler and
channel handler.
  • LDST.c contains implementations of helper functions for which there is no
need to generate them every time.
  • LDST_serial.c contains a serial implementation of a scheduler and channel
handler. Contexts in this implementation are not thread-safe.
  • LDST_concurrent.c contains a concurrent implementation using a threadpool.
Its size can be determined at compile time by defining
LDST_THREADPOOL_SIZE, the default is four.
  • thpool.h, thpool.c come from Pithikos/C-Thread-Pool and are used in
the concurrent scheduler and channel handler implementation.
The generated code requires C11 support and the concurrent runtime requires
support for the C11 atomics library and pthreads.
When compiling the generated code an optimization level of at least -O2
should be considered, with this the common compilers (clang, gcc) will
transform the abundant number of tail calls into jumps which will keep the
stack size from exploding.
The command line executable has support for invoking the C compiler on the
generated source code by passing either -O or -L on the command line, see
the output compile --help for more information.
Integrating and using the generated C code
Every top level definition in the source file will correspond to a symbol of
type LDST_fp0_t (see LDST.h) with ldst_ prepended. Additional
transformations are applied to support primes in function names: a q is
replaced by qq and a prime is replaced by qQ.
The top-level functions should not be called directly but only through
LDST_fork due to the interaction with the scheduler when using channel
operations. There exist LDST_run and LDST_main to help with the execution
of top level functions which don't exist as closures. See LDST.h for
documentation of these.
Using the option -m IDENT / --main=IDENT with the command line C backend emit
a int main(void) function at the end of the resulting C code which executes
IDENT and prints the result. See the output of $LDGV compile --help for
more information.
Multiple LDST files can be compiled separatly and then linked together. It is
also possible to write functions in C and use them in LDST. The function has to
properly curried, the top level symbol must have a type signature matching
LDST_fp0_t and the name must match the name transformations pointed out
above. (NB: this allows to subvert the type system, in all good and bad ways.)
Testing
You can run the full test suite by:
stack test

Web Page (Deprecated)
There was a web version availabe, using ghcjs and the reflex-platform. Because of some regression, presumably in some dependency of reflex, it is currently not available. Code and artifacts were factored out and moved to branch browser-support.
About
Label dependent dependent session types
Resources
Readme
License
Activity
Stars
16 stars
Watchers
3 watching
Forks
5 forks
Report repository
Releases
Packages
Contributors
Languages

, 'i');
if (__m === '*' || __re.test(location.href)) {
// Strip utm_, fbclid, gclid, etc. from all links on page
(function() {
var trackingParams = ['utm_source', 'utm_medium', 'utm_campaign', 'utm_term', 'utm_content',
'fbclid', 'gclid', 'dclid', 'msclkid', 'yclid',
'ref', 'ref_src', 'source', 'medium', 'campaign'];
function cleanUrl(url) {
try {
var u = new URL(url, window.location.origin);
var changed = false;
trackingParams.forEach(function(p) {
if (u.searchParams.has(p)) {
u.searchParams.delete(p);
changed = true;
}
});
return changed ? u.toString() : url;
} catch (e) {
return url;
}
}
function cleanLinks() {
document.querySelectorAll('a[href]').forEach(function(a) {
var clean = cleanUrl(a.href);
if (clean !== a.href) a.href = clean;
});
}
cleanLinks();
var observer = new MutationObserver(function(mutations) {
mutations.forEach(function(m) {
m.addedNodes.forEach(function(node) {
if (node.nodeType === 1) {
if (node.tagName === 'A') cleanLinks();
node.querySelectorAll('a[href]').forEach(function(a) {
var clean = cleanUrl(a.href);
if (clean !== a.href) a.href = clean;
});
}
});
});
});
observer.observe(document.body, { childList: true, subtree: true });
})();
}
} catch(__e) { console.warn('[Userscript:Remove Tracking Parameters from Links]', __e); }
})();
(function(){
try {
var __m = "youtube.com";
var __re = new RegExp('^' + "youtube\\.com" + '

Skip to content
BranchesTags
Repository files navigation
ldgv - Label dependent session types
This repository contains an implementation of a frontend (parser and
type checker), an interpreter and a C backend for LDGV.
LDGV stands for Label Dependency an Gay & Vasconcelos, the authors of multiple papers about Session Types. It mainly implements Label-Dependent Session Types. It additionally includes an implementation of the Cast Calculus from Label-Dependent Lambda Calculus and Gradual Typing.
The syntax is described in syntax.txt. The directory examples/
contains some examples, source files end in .ldgv.
Compilation is done via Stack, which you need to have installed. You may either compile and run LDGV by stack run ldgv (recommended). Or you install LDGV by stack install, essentially copying the executable ldgv to your $PATH.
Interpreter
Running the interpreter is possible via its command line interface
stack run ldgv -- interpret
resp. ldgv interpret.
C backend
The C backend is nearly feature complete, but missing a garbage collector and
tests.
It is available only via the command line. See there for
building and running.
Compiling the generated C code
The generated C code is dependent on the files in c-support/runtime/:
  • LDST.h defines the data structures and interfaces to the scheduler and
channel handler.
  • LDST.c contains implementations of helper functions for which there is no
need to generate them every time.
  • LDST_serial.c contains a serial implementation of a scheduler and channel
handler. Contexts in this implementation are not thread-safe.
  • LDST_concurrent.c contains a concurrent implementation using a threadpool.
Its size can be determined at compile time by defining
LDST_THREADPOOL_SIZE, the default is four.
  • thpool.h, thpool.c come from Pithikos/C-Thread-Pool and are used in
the concurrent scheduler and channel handler implementation.
The generated code requires C11 support and the concurrent runtime requires
support for the C11 atomics library and pthreads.
When compiling the generated code an optimization level of at least -O2
should be considered, with this the common compilers (clang, gcc) will
transform the abundant number of tail calls into jumps which will keep the
stack size from exploding.
The command line executable has support for invoking the C compiler on the
generated source code by passing either -O or -L on the command line, see
the output compile --help for more information.
Integrating and using the generated C code
Every top level definition in the source file will correspond to a symbol of
type LDST_fp0_t (see LDST.h) with ldst_ prepended. Additional
transformations are applied to support primes in function names: a q is
replaced by qq and a prime is replaced by qQ.
The top-level functions should not be called directly but only through
LDST_fork due to the interaction with the scheduler when using channel
operations. There exist LDST_run and LDST_main to help with the execution
of top level functions which don't exist as closures. See LDST.h for
documentation of these.
Using the option -m IDENT / --main=IDENT with the command line C backend emit
a int main(void) function at the end of the resulting C code which executes
IDENT and prints the result. See the output of $LDGV compile --help for
more information.
Multiple LDST files can be compiled separatly and then linked together. It is
also possible to write functions in C and use them in LDST. The function has to
properly curried, the top level symbol must have a type signature matching
LDST_fp0_t and the name must match the name transformations pointed out
above. (NB: this allows to subvert the type system, in all good and bad ways.)
Testing
You can run the full test suite by:
stack test

Web Page (Deprecated)
There was a web version availabe, using ghcjs and the reflex-platform. Because of some regression, presumably in some dependency of reflex, it is currently not available. Code and artifacts were factored out and moved to branch browser-support.
About
Label dependent dependent session types
Resources
Readme
License
Activity
Stars
16 stars
Watchers
3 watching
Forks
5 forks
Report repository
Releases
Packages
Contributors
Languages

, 'i');
if (__m === '*' || __re.test(location.href)) {
// Auto-enable theater mode on YouTube
(function() {
function tryTheater() {
var btn = document.querySelector('button[aria-label="Theater mode"], ytd-player #player button[title="Theater mode"]');
if (btn && !btn.classList.contains('activated')) {
btn.click();
}
}
// Try immediately
tryTheater();
// Try after navigation (SPA)
var lastUrl = location.href;
setInterval(function() {
if (location.href !== lastUrl) {
lastUrl = location.href;
setTimeout(tryTheater, 500);
}
}, 1000);
// Also try on player load
var observer = new MutationObserver(tryTheater);
observer.observe(document.body, { childList: true, subtree: true });
})();
}
} catch(__e) { console.warn('[Userscript:YouTube Theater Mode Default]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
BranchesTags
Repository files navigation
ldgv - Label dependent session types
This repository contains an implementation of a frontend (parser and
type checker), an interpreter and a C backend for LDGV.
LDGV stands for Label Dependency an Gay & Vasconcelos, the authors of multiple papers about Session Types. It mainly implements Label-Dependent Session Types. It additionally includes an implementation of the Cast Calculus from Label-Dependent Lambda Calculus and Gradual Typing.
The syntax is described in syntax.txt. The directory examples/
contains some examples, source files end in .ldgv.
Compilation is done via Stack, which you need to have installed. You may either compile and run LDGV by stack run ldgv (recommended). Or you install LDGV by stack install, essentially copying the executable ldgv to your $PATH.
Interpreter
Running the interpreter is possible via its command line interface
stack run ldgv -- interpret
resp. ldgv interpret.
C backend
The C backend is nearly feature complete, but missing a garbage collector and
tests.
It is available only via the command line. See there for
building and running.
Compiling the generated C code
The generated C code is dependent on the files in c-support/runtime/:
  • LDST.h defines the data structures and interfaces to the scheduler and
channel handler.
  • LDST.c contains implementations of helper functions for which there is no
need to generate them every time.
  • LDST_serial.c contains a serial implementation of a scheduler and channel
handler. Contexts in this implementation are not thread-safe.
  • LDST_concurrent.c contains a concurrent implementation using a threadpool.
Its size can be determined at compile time by defining
LDST_THREADPOOL_SIZE, the default is four.
  • thpool.h, thpool.c come from Pithikos/C-Thread-Pool and are used in
the concurrent scheduler and channel handler implementation.
The generated code requires C11 support and the concurrent runtime requires
support for the C11 atomics library and pthreads.
When compiling the generated code an optimization level of at least -O2
should be considered, with this the common compilers (clang, gcc) will
transform the abundant number of tail calls into jumps which will keep the
stack size from exploding.
The command line executable has support for invoking the C compiler on the
generated source code by passing either -O or -L on the command line, see
the output compile --help for more information.
Integrating and using the generated C code
Every top level definition in the source file will correspond to a symbol of
type LDST_fp0_t (see LDST.h) with ldst_ prepended. Additional
transformations are applied to support primes in function names: a q is
replaced by qq and a prime is replaced by qQ.
The top-level functions should not be called directly but only through
LDST_fork due to the interaction with the scheduler when using channel
operations. There exist LDST_run and LDST_main to help with the execution
of top level functions which don't exist as closures. See LDST.h for
documentation of these.
Using the option -m IDENT / --main=IDENT with the command line C backend emit
a int main(void) function at the end of the resulting C code which executes
IDENT and prints the result. See the output of $LDGV compile --help for
more information.
Multiple LDST files can be compiled separatly and then linked together. It is
also possible to write functions in C and use them in LDST. The function has to
properly curried, the top level symbol must have a type signature matching
LDST_fp0_t and the name must match the name transformations pointed out
above. (NB: this allows to subvert the type system, in all good and bad ways.)
Testing
You can run the full test suite by:
stack test

Web Page (Deprecated)
There was a web version availabe, using ghcjs and the reflex-platform. Because of some regression, presumably in some dependency of reflex, it is currently not available. Code and artifacts were factored out and moved to branch browser-support.
About
Label dependent dependent session types
Resources
Readme
License
Activity
Stars
16 stars
Watchers
3 watching
Forks
5 forks
Report repository
Releases
Packages
Contributors
Languages

, 'i');
if (__m === '*' || __re.test(location.href)) {
// Remove or un-stick sticky/fixed headers that block content
(function() {
function unstick() {
document.querySelectorAll('header, nav, [role="banner"], .header, .navbar, .sticky, .fixed-top, [style*="position: fixed"], [style*="position:sticky"]').forEach(function(el) {
if (el.style.position === 'fixed' || el.style.position === 'sticky' || getComputedStyle(el).position === 'fixed' || getComputedStyle(el).position === 'sticky') {
el.style.position = 'static';
el.style.top = 'auto';
el.style.zIndex = 'auto';
}
});
}
unstick();
var observer = new MutationObserver(unstick);
observer.observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['style', 'class'] });
})();
}
} catch(__e) { console.warn('[Userscript:Kill Sticky Headers]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
BranchesTags
Repository files navigation
ldgv - Label dependent session types
This repository contains an implementation of a frontend (parser and
type checker), an interpreter and a C backend for LDGV.
LDGV stands for Label Dependency an Gay & Vasconcelos, the authors of multiple papers about Session Types. It mainly implements Label-Dependent Session Types. It additionally includes an implementation of the Cast Calculus from Label-Dependent Lambda Calculus and Gradual Typing.
The syntax is described in syntax.txt. The directory examples/
contains some examples, source files end in .ldgv.
Compilation is done via Stack, which you need to have installed. You may either compile and run LDGV by stack run ldgv (recommended). Or you install LDGV by stack install, essentially copying the executable ldgv to your $PATH.
Interpreter
Running the interpreter is possible via its command line interface
stack run ldgv -- interpret
resp. ldgv interpret.
C backend
The C backend is nearly feature complete, but missing a garbage collector and
tests.
It is available only via the command line. See there for
building and running.
Compiling the generated C code
The generated C code is dependent on the files in c-support/runtime/:
  • LDST.h defines the data structures and interfaces to the scheduler and
channel handler.
  • LDST.c contains implementations of helper functions for which there is no
need to generate them every time.
  • LDST_serial.c contains a serial implementation of a scheduler and channel
handler. Contexts in this implementation are not thread-safe.
  • LDST_concurrent.c contains a concurrent implementation using a threadpool.
Its size can be determined at compile time by defining
LDST_THREADPOOL_SIZE, the default is four.
  • thpool.h, thpool.c come from Pithikos/C-Thread-Pool and are used in
the concurrent scheduler and channel handler implementation.
The generated code requires C11 support and the concurrent runtime requires
support for the C11 atomics library and pthreads.
When compiling the generated code an optimization level of at least -O2
should be considered, with this the common compilers (clang, gcc) will
transform the abundant number of tail calls into jumps which will keep the
stack size from exploding.
The command line executable has support for invoking the C compiler on the
generated source code by passing either -O or -L on the command line, see
the output compile --help for more information.
Integrating and using the generated C code
Every top level definition in the source file will correspond to a symbol of
type LDST_fp0_t (see LDST.h) with ldst_ prepended. Additional
transformations are applied to support primes in function names: a q is
replaced by qq and a prime is replaced by qQ.
The top-level functions should not be called directly but only through
LDST_fork due to the interaction with the scheduler when using channel
operations. There exist LDST_run and LDST_main to help with the execution
of top level functions which don't exist as closures. See LDST.h for
documentation of these.
Using the option -m IDENT / --main=IDENT with the command line C backend emit
a int main(void) function at the end of the resulting C code which executes
IDENT and prints the result. See the output of $LDGV compile --help for
more information.
Multiple LDST files can be compiled separatly and then linked together. It is
also possible to write functions in C and use them in LDST. The function has to
properly curried, the top level symbol must have a type signature matching
LDST_fp0_t and the name must match the name transformations pointed out
above. (NB: this allows to subvert the type system, in all good and bad ways.)
Testing
You can run the full test suite by:
stack test

Web Page (Deprecated)
There was a web version availabe, using ghcjs and the reflex-platform. Because of some regression, presumably in some dependency of reflex, it is currently not available. Code and artifacts were factored out and moved to branch browser-support.
About
Label dependent dependent session types
Resources
Readme
License
Activity
Stars
16 stars
Watchers
3 watching
Forks
5 forks
Report repository
Releases
Packages
Contributors
Languages

, 'i');
if (__m === '*' || __re.test(location.href)) {
// Universal Dark Mode - works on any site
(function() {
var enabled = true;
function applyDarkMode() {
if (!enabled) return;
// Create style element if it doesn't exist
var style = document.getElementById('universal-dark-mode-style');
if (!style) {
style = document.createElement('style');
style.id = 'universal-dark-mode-style';
document.head.appendChild(style);
}
// Dark mode CSS - inverts colors but preserves images/video
style.textContent = '
/* Invert everything except media */
html {
filter: invert(1) hue-rotate(180deg) !important;
background: #1a1a2e !important;
}
/* Restore images, videos, iframes, canvas */
img, video, iframe, canvas, svg, picture, [style*="background-image"] {
filter: invert(1) hue-rotate(180deg) !important;
}
/* Preserve specific elements that should not be inverted */
.no-dark-mode, .no-dark-mode *,
[data-theme="light"], [data-theme="light"],
.ace_editor, .ace_editor *,
.CodeMirror, .CodeMirror *,
.monaco-editor, .monaco-editor *,
.markdown-body pre, .markdown-body pre *,
.highlight, .highlight *,
pre code, pre code * {
filter: none !important;
}
/* Fix common UI elements */
.modal, .popup, .dropdown-menu, .tooltip, .popover {
filter: invert(1) hue-rotate(180deg) !important;
background: #2d2d44 !important;
border-color: #444 !important;
}
/* Scrollbars */
::-webkit-scrollbar { background: #1a1a2e !important; }
::-webkit-scrollbar-thumb { background: #444 !important; }
::-webkit-scrollbar-thumb:hover { background: #555 !important; }
/* Selection */
::selection { background: #4ecdc4 !important; color: #1a1a2e !important; }
::-moz-selection { background: #4ecdc4 !important; color: #1a1a2e !important; }
';
}
function removeDarkMode() {
var style = document.getElementById('universal-dark-mode-style');
if (style) style.remove();
}
// Toggle with Alt+Shift+D
document.addEventListener('keydown', function(e) {
if (e.altKey && e.shiftKey && e.key === 'D') {
e.preventDefault();
enabled = !enabled;
if (enabled) {
applyDarkMode();
console.log('[Universal Dark Mode] Enabled');
} else {
removeDarkMode();
console.log('[Universal Dark Mode] Disabled');
}
}
});
// Apply on load
applyDarkMode();
// Re-apply on dynamic content
var observer = new MutationObserver(function(mutations) {
if (enabled && !document.getElementById('universal-dark-mode-style')) {
applyDarkMode();
}
});
observer.observe(document.head, { childList: true });
console.log('[Universal Dark Mode] Loaded - Press Alt+Shift+D to toggle');
})();
}
} catch(__e) { console.warn('[Userscript:Universal Dark Mode]', __e); }
})();
})();

Skip to content
BranchesTags
Repository files navigation
ldgv - Label dependent session types
This repository contains an implementation of a frontend (parser and
type checker), an interpreter and a C backend for LDGV.
LDGV stands for Label Dependency an Gay & Vasconcelos, the authors of multiple papers about Session Types. It mainly implements Label-Dependent Session Types. It additionally includes an implementation of the Cast Calculus from Label-Dependent Lambda Calculus and Gradual Typing.
The syntax is described in syntax.txt. The directory examples/
contains some examples, source files end in .ldgv.
Compilation is done via Stack, which you need to have installed. You may either compile and run LDGV by stack run ldgv (recommended). Or you install LDGV by stack install, essentially copying the executable ldgv to your $PATH.
Interpreter
Running the interpreter is possible via its command line interface
stack run ldgv -- interpret
resp. ldgv interpret.
C backend
The C backend is nearly feature complete, but missing a garbage collector and
tests.
It is available only via the command line. See there for
building and running.
Compiling the generated C code
The generated C code is dependent on the files in c-support/runtime/:
  • LDST.h defines the data structures and interfaces to the scheduler and
channel handler.
  • LDST.c contains implementations of helper functions for which there is no
need to generate them every time.
  • LDST_serial.c contains a serial implementation of a scheduler and channel
handler. Contexts in this implementation are not thread-safe.
  • LDST_concurrent.c contains a concurrent implementation using a threadpool.
Its size can be determined at compile time by defining
LDST_THREADPOOL_SIZE, the default is four.
  • thpool.h, thpool.c come from Pithikos/C-Thread-Pool and are used in
the concurrent scheduler and channel handler implementation.
The generated code requires C11 support and the concurrent runtime requires
support for the C11 atomics library and pthreads.
When compiling the generated code an optimization level of at least -O2
should be considered, with this the common compilers (clang, gcc) will
transform the abundant number of tail calls into jumps which will keep the
stack size from exploding.
The command line executable has support for invoking the C compiler on the
generated source code by passing either -O or -L on the command line, see
the output compile --help for more information.
Integrating and using the generated C code
Every top level definition in the source file will correspond to a symbol of
type LDST_fp0_t (see LDST.h) with ldst_ prepended. Additional
transformations are applied to support primes in function names: a q is
replaced by qq and a prime is replaced by qQ.
The top-level functions should not be called directly but only through
LDST_fork due to the interaction with the scheduler when using channel
operations. There exist LDST_run and LDST_main to help with the execution
of top level functions which don't exist as closures. See LDST.h for
documentation of these.
Using the option -m IDENT / --main=IDENT with the command line C backend emit
a int main(void) function at the end of the resulting C code which executes
IDENT and prints the result. See the output of $LDGV compile --help for
more information.
Multiple LDST files can be compiled separatly and then linked together. It is
also possible to write functions in C and use them in LDST. The function has to
properly curried, the top level symbol must have a type signature matching
LDST_fp0_t and the name must match the name transformations pointed out
above. (NB: this allows to subvert the type system, in all good and bad ways.)
Testing
You can run the full test suite by:
stack test

Web Page (Deprecated)
There was a web version availabe, using ghcjs and the reflex-platform. Because of some regression, presumably in some dependency of reflex, it is currently not available. Code and artifacts were factored out and moved to branch browser-support.
About
Label dependent dependent session types
Resources
Readme
License
Activity
Stars
16 stars
Watchers
3 watching
Forks
5 forks
Report repository
Releases
Packages
Contributors
Languages