A Compiler for the Popr Language

They see me rollin'. They're Heyting. -- Chamillionaire, 2005

A place to collect work on dialectica categories.

a library for experimental linear lambda calculus

LinearOne is a prototype theorem prover for first-order (multiplicative, intuitionistic) linear logic.

Automated theorem prover for a linear logic-based calculus for molecular biology.

An implementation of interaction nets as a forth-like concatenative programming language.

a linear logic prover based on Naoyuki Tamura's llprover that works under SWI Prolog

A neurosymbolic parser for Dutch.

Session Types Library for ATS

Developing a type system for a minimal reversible functional language.

Agda formalization of the Attack Tree Linear Logic

Espèces généralisées de structures sur les groupoïdes

A latex package to draw the most general interaction nets: with multiports and multiwires (a.k.a. hyperedges)

A Haskell EDSL for conducting threat analysis using Attack Trees

Python module for (i) the representation of typelogical grammar derivations and (ii) their extraction from Lassy and Alpino-style dependency graphs.

A neural parser for typelogical grammars based on Sinkhorn networks and Linear Logic Proof Nets.

An incomplete implementation of CLASS's type system in Agda

This is a bibliography of papers using substructural logics in security