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:

[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

[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

[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

[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

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,

[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

[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 >

[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

[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:

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

[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