MechanisingBehaviouralTypes

	A	B	C	D	E	F	G	H	I	J
1	how did you deal with binders and linearity, and why?
2	Author(s)	Language	Proof Assistant	Results/Reference	Representation of binders	Pros	Cons	Approach to linearity	Pros	Cons

3	Uma Zalakain / Ornela Dardha	pi with linear, graded and shared types	Agda	https://arxiv.org/abs/2005.05902	type level de Bruijn indices	well-scoped by construction, easily mechanised	not immediately human-friendly	leftover typing on partial commutative monoids	no extrinsic context splits	needs to be cancelative
4	James Wood / Robert Atkey	λR / simple quantitative type theory	Agda	https://arxiv.org/abs/2005.02247	tree-shaped de Bruijn indices	metatheory just like STλC, no green slime	unreadable	semiring usage annotations	requires only standard linear algebra operations	no clear general approach to usage checking, users have to supply linear algebra proofs
5	Robert Atkey	linear STλC	Agda	https://github.com/bobatkey/sorting-types/blob/master/agda/Linear.agda	co-de Bruijn indices	particularly simple in the linear case, readily translated to BCI combinators	even more unreadable than de Bruijn indices	linear co-de Bruijn indices	no algebra	doesn't readily generalise away from syntactic linearity, users have to supply permutations
6	Luca Ciccone / Luca Padovani	linear pi calculus with dependent pairs	Agda	https://gitlab.di.unito.it/luca.padovani/DependentLinearPi	de Brujin indices with Agda-binders in types	Agda functions can compute processes from received messages	somewhat heavy notation, inference possible but only to some extent	semiring usage annotations (one for each input/output capability)	channel types always splittable, pairs strictly linear	writing terms and processes by hand is extremely tedious
7	Guillaume Allais	MALL	Agda	https://drops.dagstuhl.de/opus/volltexte/2018/10049/	de Bruijn	Standard de Bruijn	Standard de Bruijn	I/O model to track usages of variables	Easy to adapt to a type checking algorithm	Seems limited to MALL, doesn't handle exponentials
8	Uma Zalakain / Ornela Dardha	pi with binary session types	Coq	http://www.dcs.gla.ac.uk/~ornela/projects/Uma%20Zalakain.pdf	polymorphic HOAS	transparent to the user	cannot reason about in host language	predicate on processes with polymorphic channels	trivial to define	user loses access to channel type info
9	Adrian Francalanza / Marco Giunti / António Ravara	linear pi	Coq	paper submitted	unique identifiers	names are identifiers (constants), all different (like Barendregts convention, but preserved by reduction); only one reduction rule needs adjusting (comm on replicated names generates fresh identifiers and renames the process template) and extension of names is exclusively localised to this rule (and the contextual rules that use it)	(we do with this support, but other applications might need that)	Addition and subtraction of capabilities as relations on types; addition (combination) of type environments as a relation that reduces to addition on types and is controlled by a well-formedness property	operations on types are partial functions, natural to implement	as type environments are lists that should be maps, insertion needs to be controlled to ensure they are still maps; some degree of non-determinism in the type system complicates soundness proofs
10	Enrico Tassi / Cinzia Di Giusto	linear pi	Coq		de Bruijn levels			Addition and subtraction of capabilities as relations on types; addition (combination) of type environments as a relation that reduces to addition on types and is controlled by a well-formedness property
11	Jonas Kastberg Hinrichsen / Daniël Louwrink / Robbert Krebbers / Jesper Bengtson	ML-like language + async affine binary message passing + message/term polymorphism + equi-recursive recursive types + references + copy types + locks	Coq/Iris	https://iris-project.org/pdfs/2020-actris2-submission.pdf	Coq-binders in types, strings in terms	Binders in types feel like HOAS, no meta theory needed	Relies on the semantic approach to type systems	Separation logic (Iris)	Resource reasoning encapsulated	No so clear how to do other properties than safety (e.g., deadlock)
12	Petros Papapanagiotou	pi calculus & CP	HOL Light	CP on GiHub	syntactic w/ custom substitution (Cf. Melham)	quick & easy, no libraries required	nightmare to reason about	Linear Logic	Correct-by-construction	allowed patterns severely limited
13	Edwin Brady	Idris	Idris	https://www.type-driven.org.uk/edwinb/idris-2-quantitative-type-theory-in-action.html	de Bruijn indices with proof of context membership in types	well-scoped by construction, type-driven implementation of context manipulation	Sometimes costly at compile-time	Quantitative Type Theory	Session types definable directly	"Read only" operations are syntactically noisy
14	Jan de Muijnck-Hughes, Edwin Brady, & Wim Vanderbauwhede	Idris	Idris	https://doi.org/10.4204/EPTCS.291.5	de Bruijn indicies with proof of context membership in types.	well-scoped by construction, type-driven implementation of context manipulation	Sometimes costly at compile-time	resource dependent type-system.	Safe-Value-dependent session descriptions.	Still working on projection.
15	Kirstin Peters	pi with multiparty session types	Isabelle/HOL		Nominal Sets	binders are used similar to paper proofs	requires equivariance proofs
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100