Hi Nik, Thanks for your thoughtful answer. That was what I was looking for.
Best, Bas On Fri, Jun 29, 2018 at 5:04 PM, Nikhil Swamy <nsw...@microsoft.com> wrote: > Hi Bas, > > We've made several attempts at formalizing various fragments of F*, none of > which establish consistency of the full language (unsurprisingly). > > Our most recent attempt is in a paper at POPL 2017: > https://www.fstar-lang.org/papers/dm4free/ > > There, we present a calculus called Explicitly Monadic F* (EMF*) which > includes the pure fragment of F*, with dependent types, refinement types and > user-defined monadic effects. EMF* excludes many F* features too (especially > the following, which are particularly relevant for consistency): > > 1. inductive types and pattern matching > 2. F*'s let-rec primitive (and its semantic termination check) > 3. a typing rule that supports type conversion based on provable equality > 4. divergence encapsulated in another effect > 5. the encoding of F*'s logic to first-order logic provided by an SMT solver > > For this limited EMF* calculus, we have a syntactic metatheory proving total > correctness of the WP-based program logic we derive for effectful terms. > Extending EMF* at least with features 1, 2, and 3 above and studying its > consistency would be very interesting ... well, at least to the few of us who > work on F*. > > That said, the main theorem of this POPL '17 paper is to establish the > correctness of a CPS-based transformation to derive WP calculi from > definitions of a monad. This is done by a logical relations proof on EMF*. > > Other papers have attempted to study some of these other consistency-related > features of F* in slightly different settings: > -- https://www.fstar-lang.org/papers/mumon/ this one includes a proof of > normalization of a small calculus ("pico F*") with recursion, refinement > types and our termination check > -- This short paper > https://hatt2016.inria.fr/files/2016/06/HaTT_2016_paper_1-5.pdf formalizes a > core of F*'s encoding to first-order logic > > Aside from all this, there's the question of the correctness of F*'s > implementation: of course, F* is under active development and we find, fix > and (sadly) introduce correctness bugs from time to time. We hope someday to > revisit our work on "self-certification" > (https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/popl2012-paper211.pdf) > and apply a technique like it to the current implementation of F*. > > Hope that helps, > Nik > >> -----Original Message----- >> From: fstar-club <fstar-club-boun...@lists.gforge.inria.fr> On Behalf Of Bas >> Spitters via fstar-club >> Sent: Friday, June 29, 2018 3:30 AM >> To: fstar-club@lists.gforge.inria.fr >> Subject: [fstar-club] Consistency of F-star ? >> >> What are the current conjectures, thoughts about the consistency/semantics >> of F*? >> >> Could you point me to a paper I should read? >> >> Thanks, >> >> Bas >> _______________________________________________ >> fstar-club mailing list >> fstar-club@lists.gforge.inria.fr >> https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.gf >> orge.inria.fr%2Fmailman%2Flistinfo%2Ffstar- >> club&data=02%7C01%7Cnswamy%40microsoft.com%7C428fa932a4c04 >> d1ce84708d5ddabaec4%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0% >> 7C636658651809180794&sdata=EEKoy3UGxk%2BOKuLGPDTQb%2F0AZ >> %2FhMKcc7PzI09bvk5Og%3D&reserved=0 _______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
