issues
search
jonsterling
/
JonPRL
An proof refinement logic for computational type theory. Inspired by Nuprl. [For up-to-date development, see JonPRL's successor, RedPRL: https://github.com/redprl/sml-redprl]
http://www.jonprl.org
MIT License
109
stars
9
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Broken links
#254
arthuraa
closed
4 years ago
2
fix a binding bug in Subst rule
#253
jonsterling
closed
7 years ago
0
A Module System?
#252
markfarrell
opened
8 years ago
0
Formalization of Cubical Type Theory
#251
markfarrell
opened
8 years ago
2
Add universe hierarchy
#250
jonsterling
closed
8 years ago
1
Internally prove whether or not "axiom K" can be derived?
#249
markfarrell
closed
8 years ago
2
Types are ∞-groupoids
#248
markfarrell
closed
8 years ago
2
Try JonPRL
#247
markfarrell
opened
8 years ago
5
Upgrade sml-telescopes to master
#246
jonsterling
closed
8 years ago
0
consider switching to "dependent LCF" refiner
#245
jonsterling
opened
8 years ago
2
Fix functionality bug; change per type arity
#244
jonsterling
closed
8 years ago
1
Respect for Functionality
#243
jozefg
closed
8 years ago
7
Consider switching to typed ABTs
#242
jonsterling
opened
8 years ago
5
switch per operator signature to (2)
#241
jonsterling
closed
8 years ago
2
Fixed eqcd to not run Eq.Eq with no gas
#240
jozefg
closed
8 years ago
1
Better error messages
#239
jonsterling
opened
8 years ago
0
`auto` tactic can crash
#238
peterohanley
closed
8 years ago
3
Standard eq-eq rule is not invertible
#237
jonsterling
closed
8 years ago
1
Start developing Synthetic Topology
#236
jonsterling
closed
8 years ago
2
Correctly handle wildcards so that unification works with binders
#235
jozefg
closed
8 years ago
2
Simplified inconsistent DecideEq rule
#234
jozefg
closed
8 years ago
6
DecideEq is broken
#233
jozefg
closed
8 years ago
2
Begin tagging versions / releases
#232
jonsterling
closed
8 years ago
1
Document containers, trees, extensions, neighborhoods, etc.
#231
jonsterling
opened
8 years ago
0
Fixed #229 by properly implementing relativize
#230
jozefg
closed
8 years ago
1
Configuration files don't support "/"
#229
jonsterling
closed
8 years ago
1
Proof that typing is undecidable
#228
jozefg
closed
8 years ago
3
Per
#227
vrahli
closed
8 years ago
6
Importing libraries
#226
vrahli
closed
8 years ago
5
Added a proof that all polymorphic functions A -> A are id
#225
jozefg
closed
8 years ago
12
Added a proof of the impossibility of halting oracle in JonPRL and bugfix
#224
jozefg
closed
8 years ago
0
Added stopgap fix for #214
#223
jozefg
closed
8 years ago
1
Canonical-forms tests
#222
jonsterling
opened
8 years ago
0
Container improvements; add neighborhoods (i.e. finite approximations)
#221
jonsterling
closed
8 years ago
1
improvements to container theory
#220
jonsterling
closed
8 years ago
0
Are the Image rules sound? [Question]
#219
jonsterling
closed
8 years ago
2
Make JonPRL SML '97 Compatible
#218
jozefg
opened
8 years ago
7
Made tactic definitions late-bind the world they use (closes #216)
#217
jozefg
closed
8 years ago
4
"late binding" for resource tactic
#216
jonsterling
closed
8 years ago
0
higher-order judgments
#215
jonsterling
closed
8 years ago
1
pattern compilation is broken for multiple bindings
#214
jonsterling
opened
8 years ago
17
quotients and PER types
#213
jonsterling
closed
8 years ago
7
Made sure to use recursive comments (currently broken in parcom)
#212
jozefg
closed
8 years ago
0
Custom resources
#211
jozefg
closed
8 years ago
5
Start adding containers & their trees
#210
jonsterling
closed
8 years ago
1
User Defined Resources
#209
jozefg
closed
8 years ago
1
Targeted Reduce and Unfold
#208
jozefg
opened
8 years ago
1
WF tactic improvements
#207
jonsterling
closed
8 years ago
0
Add support for new PRUNE tactical
#206
jonsterling
closed
8 years ago
0
Added a tactic to run the registered tactics for a resource
#205
jozefg
closed
8 years ago
1
Next