Changes between Version 17 and Version 18 of NewAxioms/Nonlinearity


Ignore:
Timestamp:
May 30, 2013 3:12:39 PM (11 months ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/Nonlinearity

    v17 v18  
    3434 
    3535(Interestingly, proofs of the soundness of the existing system have been published. For example, see [http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/fc-tldi.pdf here] and [http://www.cis.upenn.edu/~stevez/papers/WVPJZ11.pdf here]. These proofs are not necessarily incorrect, but they implicitly don't allow nonlinear family instances.) 
     36 
     37Conor's alternative general idea: 
     38 * '''when performing the overlap check, during unification succeed (instead of failing) if the occurs check happens''' 
    3639 
    3740