issues
search
atlanmod
/
coqtl
CoqTL allows users to write model transformations and prove engine/transformation correctness in Coq
Other
13
stars
12
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Use prebuilt dev container image
#110
TheoLeCalvar
closed
2 years ago
0
Add dev container setup for VS Code
#109
TheoLeCalvar
closed
2 years ago
0
Change order of arguments in lambda functions in Syntax
#108
massimotisi
opened
2 years ago
0
No link
#107
massimotisi
closed
2 years ago
0
Trace links as a function
#106
massimotisi
opened
2 years ago
0
Removing core/test
#105
massimotisi
closed
2 years ago
0
Updating README
#104
massimotisi
closed
2 years ago
0
No link
#103
massimotisi
closed
2 years ago
0
Proofs for parallelizable semantics
#102
massimotisi
closed
3 years ago
0
Expr and evalExpr should be in a separate typeclass
#101
veriatl
opened
3 years ago
0
using sumtype for metamodel.v
#100
veriatl
closed
2 years ago
0
a typeclass for ConcreteSyntax, containing just parse
#99
veriatl
opened
3 years ago
0
Seperate Metamodel.v from Engine.v
#98
veriatl
closed
2 years ago
0
Simple
#97
massimotisi
closed
3 years ago
0
refactor engine and proof
#96
veriatl
closed
3 years ago
0
parameter tr is not needed in applyLinkOnPatternTraces
#95
veriatl
opened
3 years ago
0
update license and readme
#94
veriatl
closed
3 years ago
0
Update Interpreter.v
#93
veriatl
closed
3 years ago
0
Fix in EngineTwoPhase.v
#92
veriatl
closed
3 years ago
0
Reintroduce option in syntax for output pattern element
#91
massimotisi
opened
3 years ago
0
Improve interface for expression evaluator
#90
massimotisi
closed
2 years ago
0
Certification
#89
veriatl
closed
3 years ago
0
Two-Phase Semantics
#88
massimotisi
closed
3 years ago
0
Simple
#87
massimotisi
closed
3 years ago
0
Tactic for case analysis on rules
#86
massimotisi
opened
4 years ago
1
In concrete syntax links could be specified by computing only their target elements in the lambda
#85
massimotisi
opened
4 years ago
0
Notation for bring input pattern types and lambda variables closer
#84
massimotisi
opened
4 years ago
0
Removed coercions
#83
massimotisi
closed
4 years ago
0
Project cleanup
#82
massimotisi
closed
4 years ago
1
documentation
#81
veriatl
closed
4 years ago
0
Concrete Syntax
#80
massimotisi
closed
4 years ago
0
Split Metamodel typeclass into two instances of Sum
#79
massimotisi
closed
2 years ago
0
Inferring InTypes for buildConcreteOutputPatternElement
#78
massimotisi
opened
4 years ago
1
denoteModelClass ColumnClass != Column
#77
massimotisi
closed
2 years ago
0
Simple
#76
massimotisi
closed
4 years ago
0
Simple
#75
massimotisi
closed
4 years ago
0
Master
#74
veriatl
closed
4 years ago
0
Unable to make the project
#73
luntan-maker
closed
2 years ago
4
Computational
#72
massimotisi
closed
4 years ago
0
Leaf lemmas with do notation
#71
jhtr
closed
4 years ago
0
Patch for Issues #52 and #51
#70
veriatl
closed
4 years ago
0
Add scripts for compiling and generate metrics and documentations
#69
massimotisi
closed
4 years ago
1
Split user proofs for readability and metrics
#68
veriatl
closed
4 years ago
0
new theorem proved
#67
veriatl
closed
4 years ago
0
new theorems of C2R and HSM2FSM
#66
veriatl
closed
4 years ago
0
Information preservation proof
#65
jhtr
closed
4 years ago
0
new proof in C2R
#64
veriatl
closed
4 years ago
0
Split CoqTL in three modules
#63
jhtr
closed
4 years ago
0
Port simple proofs to the typeclass
#62
jhtr
closed
4 years ago
1
Patch for issue#52
#61
veriatl
closed
4 years ago
0
Next