issues
search
jaccokrijnen
/
plutus-cert
0
stars
2
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Why does binds_Gamma not add the real constructor types?
#55
jaccokrijnen
closed
2 months ago
2
Simplify definition of contextual equivalence?
#54
jaccokrijnen
opened
2 months ago
0
Remove type annotations from Error?
#53
jaccokrijnen
opened
4 months ago
0
Typing rules: IWrap Unwrap should check that the new X is fresh (or does not capture)
#52
jaccokrijnen
opened
5 months ago
0
Port to Coq 8.18 WIP
#51
jaccokrijnen
opened
7 months ago
1
Generated decision procedure for uniqueness runs in quadratic time
#50
jaccokrijnen
opened
9 months ago
0
Various fixes
#49
michaelpj
closed
9 months ago
0
Improve extracted haskell and glue code
#48
jaccokrijnen
opened
10 months ago
1
Postulate normalisation function
#47
jaccokrijnen
opened
10 months ago
0
Comparing notions of equivalence
#46
jaccokrijnen
opened
10 months ago
0
Proof sketches for correctness of translation relations
#45
jaccokrijnen
opened
10 months ago
0
Meauring cost of extracted decision procedures
#44
jaccokrijnen
opened
10 months ago
3
Add submodule in plutus and depend on plutus-cert cabal package
#43
jaccokrijnen
opened
10 months ago
0
New dead code spec and LetRec
#42
jaccokrijnen
closed
4 months ago
1
Dead code specification using uniqueness and well-scoped
#41
jaccokrijnen
opened
11 months ago
3
Add lazily bound terms (non-strict) to RG
#40
jaccokrijnen
opened
11 months ago
1
Split up Semantics.Multisubstitution.Congruence
#39
jaccokrijnen
opened
11 months ago
0
Define `RC` and `RV` with mutual recursion
#38
jaccokrijnen
opened
11 months ago
0
Change `value` to `result`
#37
jaccokrijnen
opened
11 months ago
0
Dead code correctness
#36
jaccokrijnen
opened
1 year ago
0
LetNonStrict: introduced lambda variable must be fresh
#35
jaccokrijnen
opened
1 year ago
0
Syntax for defining relations as partial functions?
#34
jaccokrijnen
opened
1 year ago
0
Contexts with more information than just typing
#33
jaccokrijnen
opened
1 year ago
0
Update Beta spec
#32
jaccokrijnen
opened
1 year ago
0
Normal form for scope-related passes
#31
jaccokrijnen
opened
1 year ago
0
Plutus core and CEK machine
#30
jaccokrijnen
opened
1 year ago
1
Logical relation vs (bi)simulation
#29
jaccokrijnen
opened
1 year ago
0
Factor out built-ins
#28
jaccokrijnen
opened
1 year ago
0
Todos SCP paper code
#27
jaccokrijnen
closed
10 months ago
0
Rename flatten to revconcat
#26
jaccokrijnen
opened
1 year ago
0
Move ContextInvariance.AFI.closed to Analysis
#25
jaccokrijnen
opened
1 year ago
0
Big-step: letrec is now always non-strict
#24
jaccokrijnen
opened
1 year ago
0
Environment-based vs substitution-based semantics
#23
jaccokrijnen
opened
1 year ago
0
Implement type checker and type normalizer
#22
jaccokrijnen
opened
1 year ago
0
Rename Cong (congruence) to Compat (compatible)
#21
jaccokrijnen
closed
10 months ago
0
Dead code correctness: how to prove strictly bound variables will always be a value
#20
jaccokrijnen
opened
1 year ago
1
Use-case for folds/attribute grammars: efficient rename decision procedure
#19
jaccokrijnen
opened
1 year ago
1
Could some semantic equivalence proofs be simpler?
#18
jaccokrijnen
closed
10 months ago
0
Enforce unique scoping in Typing of Let Rec
#17
jaccokrijnen
opened
1 year ago
0
Shadowing of type variables is problematic in static semantics
#16
jaccokrijnen
opened
1 year ago
5
Typing of Error ignores the type annotation on it, so big-step is type-preserving
#15
jaccokrijnen
opened
1 year ago
1
Escaping ADTs and typability
#14
jaccokrijnen
opened
1 year ago
2
Definition of static semantics preservation
#13
jaccokrijnen
opened
1 year ago
0
Big-step: support datatypes ADTS
#12
jaccokrijnen
opened
1 year ago
5
Big-step: support non-strict let bindings
#11
jaccokrijnen
opened
1 year ago
1
Don't dump arity of constructors anymore
#10
jaccokrijnen
opened
1 year ago
0
Can we avoid neutral terms for built-ins?
#9
jaccokrijnen
opened
1 year ago
3
Representation of Γ and Δ
#8
jaccokrijnen
closed
10 months ago
0
Is Kind_Base premise in T_Let (has_type) necessary?
#7
jaccokrijnen
opened
1 year ago
0
Thesis/semantic equivalence step index
#6
jorisdral
closed
2 years ago
0
Next