Changes between Version 17 and Version 18 of NewAxioms/Nonlinearity


Ignore:
Timestamp:
May 30, 2013 3:12:39 PM (2 years 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