[fstar-club] PhD positions on refinement types at Inria Rennes

Dear F* folks, Jean-Pierre Talpin, one of our Inria colleagues who is located in Rennes (in CC), is looking for PhD students on several refinement types projects that could include the use of F* and Low*. If you know anyone who could be interested in this please let them know. Regards, Catalin P

Re: [fstar-club] Proving that a function is equal to its definition

Reminds be of an issue I filed really long time ago: https://github.com/FStarLang/FStar/issues/121 On Mon, May 15, 2017 at 4:00 PM, Clément Pit-Claudel via fstar-club wrote: > Hi all, > > I'm having trouble with the (simplified) example below. Is there a subtle > type-inference-related reason

Re: [fstar-club] Proving that a function is equal to its definition

Hi Clément, Did a quick experiment with Kenji, and we could easily prove your lemma using assert_norm: let unfold_tos (s: nat) : Lemma (trees_of_size s == (if s = 0 then [Leaf] else List.Tot.concatMap #(p: (nat * nat){(fst p) + (snd p) == s

Re: [fstar-club] Proving that a function is equal to its definition

>> Did a quick experiment with Kenji, and we could easily prove your >> lemma using assert_norm: >> … > > Wonderful, thanks! Works like a charm. > This might be a useful addition to the tutorial :) Or did I miss it? Added this to the wiki for now: https://github.com/FStarLang/FStar/wiki/Using-SMT-

Re: [fstar-club] PhD positions on refinement types at Inria Rennes

Jean-Pierre lets us know that he is still looking for an excellent master student to start a PhD in Rennes on the following topics (in French, sorry). TRACK: typage par raffinement et algébre de contrats des kernels modulaires Un système cyber-physique (automobile, avionique, automatisme industr

[fstar-club] F* v0.9.5.0 released!

v0.9.5.0 [image: @nikswamy] nikswamy released this 10 hours ago This is another big release with lots of changes and new features compared to v0.9.4.0 Main new features - Proofs by reification (see this p

Re: [fstar-club] A few random questions

Hi Julien, Thank you for your questions. Since the set of people who can answer all these questions at once is rather small, I'll try to answer some, hoping that others will add to this. On Sun, Sep 17, 2017 at 7:53 PM, Julien Cretin via fstar-club < fstar-club@lists.gforge.inria.fr> wrote: > Hi

Re: [fstar-club] A few random questions

> > I guess we can't avoid the trick of taking a heap as argument and > requiring that it is equal to the real heap. Ideally I would have expected > something like: > > val zero: x: ref nat -> ST unit > (requires (fun h -> contains h x)) > (ensures (fun h0 r h1 -> modifies (only x) h0 h1 /\

[fstar-club] Fwd: [fmics] Two PhD offers at Inria, Rennes, on refinement types for system design

Jean-Pierre Talpin (in CC) is looking for PhD students at Inria Rennes on projects that could involve a non-trivial amount of F* :) *De :* fmics-requ...@inria.fr [mailto:fmics-requ...@inria.fr] *De la part de* Jean-Pierre Talpin *Envoyé :* vendredi 9 mars 2018 09:50 *À :* fm...@inrialpes.fr *Obj

[fstar-club] Summer schools on F*/Low* coming up in May

Dear F* folks, There are a couple of summer schools coming up soon that include short courses on F* and Low*: - EPIT 2018 Software Verification Spring School (https://projects.lsv.fr/epit18/) - Eighth Summer School on Formal Techniques (http://fm.csl.sri.com/SSFT18/) Registration for EPIT has rec

[fstar-club] F* v0.9.6.0 released

Dear F* users, We are pleased to announce that F* v0.9.6.0 was released last week: https://github.com/FStarLang/FStar/releases/tag/v0.9.6.0 A large number of people contributed to this release: thanks to all! # Main new features - Meta-F*: A metaprogramming and tactic framework, as described in

[fstar-club] PostDoc positions at Inria Paris on F* and on Formally Secure Compilation

Hello everyone, 2 PostDoc positions are available in my group at Inria Paris on the F* and ERC SECOMP projects. I am seeking exceptional candidates with a strong, internationally competitive research track record. On F* (https://www.fstar-lang.org/), I am looking for someone with research experti

[fstar-club] Chatting about F* on Zulip

Hi everyone, We recently set up a Zulip instance for chatting about F* or asking questions. Please help us try it out: https://fstar.zulipchat.com Zulip (https://zulipchat.com) is an open source alternative to Slack that offers good organization features, which should allow switching between sync

[fstar-club] 1st CFP for Certified Programs and Proofs (CPP 2020)

**1st CFP for Certified Programs and Proofs (CPP 2020)** Certified Programs and Proofs (CPP) is an international conference on practical and theoretical topics in all areas that consider certification as an essential paradigm for their work. Certification here means formal, mechanized verification

Re: [fstar-club] FStar school

Hi Marc, Not sure about the "in depth" part, but otherwise there are 2 summer schools that will have F* courses coming up soon: * The Oregon Programming Languages Summer School, Eugene, OR, USA - Application Deadline: April 15, School: June 17-29 * Summer School on Verification Technology, Syste

[fstar-club] Fwd: VTSA'19 Luxembourg: call for applications

--- Application deadline (extended): May 17, 2019 Notification of acceptance (extended): May 20, 2019 --- UniGR Summer School on Verification Technology, Systems and Applications (VTSA 2019) July 1-5,

Re: [fstar-club] INSTALL.md

Hi Paul, Don't think this duplication is useful for anything. Let's remove it: https://github.com/FStarLang/FStar/pull/1801 Catalin On Tue, Jul 2, 2019 at 10:45 AM paul zimmermann via fstar-club wrote: > >Hi, > > on > https://github.com/FStarLang/FStar/blob/master/INSTALL.md#building-f

[fstar-club] CFP for Certified Programs and Proofs (CPP 2020)

## CFP for Certified Programs and Proofs (CPP 2020) ## Certified Programs and Proofs (CPP) is an international conference on practical and theoretical topics in all areas that consider certification as an essential paradigm for their work. Certification here means formal, mechanized verification o

[fstar-club] Call for participation for CPP 2020

**Call for Participation** **Certified Programs and Proofs (CPP 2020)** - Early registration deadline: 18 December 2019 - Getting a visa: https://popl20.sigplan.org/attending/Visa - Registration: https://popl20.sigplan.org/attending/Registration - Accommodation: https://popl20.sigplan.org/

Re: [fstar-club] bug report (wrong cast from I32)

Dear Paul and Felix, Guido has just fixed https://github.com/FStarLang/FStar/issues/1803 by doing a big cleanup to the way we do machine integers in F*: https://github.com/FStarLang/FStar/pull/1850 Please have another look and sorry for the inconvenience. Regards, Catalin On Wed, Jul 3, 2019 a

[fstar-club] Fwd: Quicksort in the tutorial

-- Forwarded message - From: Shenghao Date: Tue, Aug 11, 2020 at 9:44 AM Subject: Quicksort in the tutorial To: Hello, I'm doing exercises in the tutorial ( a F* newbie). In section 6.1.2 Specifying sort, val sort_tweaked: l:list int -> Tot (m:list int{sorted m