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

[idea] implement neel's linear type system #195

Open jonsterling opened 9 years ago

jonsterling commented 9 years ago

http://www.cs.cmu.edu/~neelk/dlnl-paper.pdf

Neel formulates his type system in Harper's style, so it seems like it should be possible to implement it in JonPRL.

Basically, the linear type system is explained by PERs on machine configurations that respect linear evaluation (as opposed to PERs on expressions that respect intuitionistic evaluation). Adding this stuff may cause some initial complication, but it actually looks like it may not be too terrible. The plus side is that it would give us a way to do imperative programming directly in JonPRL's computation system, rather than the Coq-style approach of encoding a closed imperative programming language and reasoning metamathematically about its terms.

@freebroccolo What do you think?

ghost commented 9 years ago

Sorry I missed this somehow.

Implementing Neel's stuff in JonPRL would be pretty amazing :) I'd definitely be interested in that. I need to read the paper again though. As I recall, there was also supposed to be some overlap with the categorical stuff I linked you to awhile back and when I was messing with the Grothendieck stuff…

jonsterling commented 9 years ago

@freebroccolo Yeah, this would be super cool... I need to do a prototype or something; it's pretty clear to me how to type-check a linear lambda calculus, but writing a refiner for one may be a bit different from what I'm used to.