Skip to content

Commit c7c19a1

Browse files
authored
Problems I'd like to read about first
1 parent 2fe8feb commit c7c19a1

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

PROBLEMS.md

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Proof Organization and Scalability
1111
- constructs (type classes, modules, canonical structures, ...)
1212
- encodings of structures (graphs as hypermaps, numbers as Church numerals, ...)
1313
- proof object management (generation, size, ...)
14+
- proof design principles (including domain-specific ones) [Talia]
1415
- proofs by reflection vs. proofs by tactics
1516
- proof languages (Isar, C-zar, ssreflect, ...)
1617
- tactic languages (Ltac, Ltac2, Rtac, Mtac, ...)
@@ -27,8 +28,8 @@ Practical Proof Development and Evolution
2728
- library packaging and versioning
2829
- opaqueness and proof irrelevance in practice
2930
- broken proofs in new proof assistant versions
30-
- evolution-proof proofs
31-
- proof repair
31+
- evolution-proof proofs [Talia]
32+
- proof repair [Talia]
3233
- change impact analysis (incl. Ltac)
3334
- regression proof selection
3435
- regression proof prioritization

0 commit comments

Comments
 (0)