[fstar-club] Fwd: Quicksort in the tutorial

[Catalin Hritcu via fstar-club]

-- 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 /\ (forall i.
mem i l = mem i m)})
(decreases (length l))let rec
sort_tweaked l = match l with
  | [] -> []
  | pivot :: tl ->
let hi', lo' = partition (cmp pivot) tl in
partition_lemma (cmp pivot) tl;
let hi = sort_tweaked hi' in
let lo = sort_tweaked lo' in
append_mem lo (pivot :: hi);
sorted_concat_lemma lo hi pivot;
append lo (pivot :: hi)

I find it fails to compile when I replace the refinement type

"m:list int{sorted m /\ (forall i. mem i l = mem i m)}" with "m:list int{
sorted m}", just deleting the latter property. The terminal reports:

"(Error 19) assertion failed"

How can I compile the new version successfully? Could you please
give me some suggestions? Thanks a lot!

Best wishes,

-- 
Shenghao Yuan

College of Computer Science and Technology  (CCST)

Nanjing University of Aeronautics and Astronautics  (NUAA)

Nanjing China
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club

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

[Catalin Hritcu via fstar-club]

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 at 8:04 AM paul zimmermann via fstar-club
 wrote:
>
>Dear Jonathan,
>
> > From: Jonathan Protzenko 
> > Date: Wed, 3 Jul 2019 05:30:37 +
> >
> > Hello Paul and Félix,
> >
> > Thanks for the bug report -- I've filed
> > https://github.com/FStarLang/FStar/issues/1803
> >
> > Out of curiosity, what was your initial interest in F*? Are you interested 
> > in proving
> > some numerical routines?
> >
> > Cheers,
> >
> > ~ jonathan
>
> thank you. We try to prove some routines from the GNU MPFR library,
> following work started by Jianyang Pan last year, with the help of Karthik.
>
> Best regards,
> Paul Zimmermann
> ___
> fstar-club mailing list
> fstar-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club

[fstar-club] Call for participation for CPP 2020

[Catalin Hritcu via fstar-club]

**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/venue/POPL-2020-venue

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 of some sort, preferably
with the production of independently checkable certificates.
CPP spans areas of computer science, mathematics, logics, and education.

CPP 2020 will be held on 20-21 January 2020 in New Orleans, Louisiana,
United States and will be co-located with POPL 2020. CPP 2020 is
sponsored by ACM SIGPLAN, in cooperation with ACM SIGLOG.

For more information about this edition and the CPP series, please
visit https://popl20.sigplan.org/home/CPP-2020

### Invited Speakers

Adam Chlipala (MIT CSAIL) and Grigore Rosu (UIUC and Runtime Verification)

### Accepted papers

The list of accepted papers is available at
https://popl20.sigplan.org/home/CPP-2020#event-overview

### Conference dinner

This year CPP will feature a (highly subsidized) conference dinner in a
local restaurant for which we encourage you to sign up when registering
by choosing the CPP+ option.

This is possible thanks to our generous industrial supporters (list still
expected to grow a bit): https://popl20.sigplan.org/home/CPP-2020#About

### Contact

For any questions please contact the PC chairs:
Jasmin Blanchette ,
Catalin Hritcu 
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club

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

[Catalin Hritcu via fstar-club]

## 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 of some sort, preferably
with the production of independently checkable certificates.
CPP spans areas of computer science, mathematics, logic, and education.

CPP 2020 will be held on 20-21 January 2020 in New Orleans, Louisiana,
United States and will be co-located with POPL 2020. CPP 2020 is
sponsored by ACM SIGPLAN, in cooperation with ACM SIGLOG.

For more information about this edition and the CPP series please visit:
https://popl20.sigplan.org/home/CPP-2020

### News

- Submission guideline news: **lightweight double-blind reviewing process**
  and **unrestricted appendices** that don't count against the page limit

- Delighted to announce that the **invited speakers** for CPP 2020 will be:
  Adam Chlipala (MIT CSAIL) and Grigore Rosu (UIUC and Runtime Verification)

- CPP 2020 will also host the **POPLmark 15 Year Retrospective Panel**

### Important Dates

   - Abstract Deadline: 16 October 2019 at 23:59 AoE (UTC-12h)
   - Paper Submission Deadline: 21 October 2019 at 23:59 AoE (UTC-12h)
   - Notification: 27 November 2019
   - Camera Ready Deadline: 20 December 2019
   - Conference: 20 - 21 January 2020

Deadlines expire at the end of the day, anywhere on earth. Abstract
and submission deadlines are tight and there will be **no extensions**.

### Topics of Interest

We welcome submissions in research areas related to formal
certification of programs and proofs. The following is a
non-exhaustive list of topics of interests to CPP:

   - certified or certifying programming, compilation, linking, OS
 kernels, runtime systems, and security monitors;
   - certified mathematical libraries and mathematical theorems;
   - proof assistants (e.g, ACL2, Agda, Coq, Dafny, F*, HOL,
 HOL-Light, Idris, Isabelle, Lean, Mizar, Nuprl, PVS, etc)
   - new languages and tools for certified programming;
   - program analysis, program verification, and program synthesis;
   - program logics, type systems, and semantics for certified code;
   - logics for certifying concurrent and distributed systems;
   - mechanized metatheory, formalized programming language semantics,
 and logical frameworks;
   - higher-order logics, dependent type theory, proof theory,
 logical systems, separation logics, and logics for security;
   - verification of correctness and security properties;
   - formally verified blockchains and smart contracts;
   - certificates for decision procedures, including linear algebra,
 polynomial systems, SAT, SMT, and unification in algebras of interest;
   - certificates for semi-decision procedures, including equality,
 first-order logic, and higher-order unification;
   - certificates for program termination;
   - formal models of computation;
   - mechanized (un)decidability and computational complexity proofs;
   - user interfaces for proof assistants and theorem provers;
   - original formal proofs of known results in math or computer science;
   - teaching mathematics and computer science with proof assistants.

### Program Committee Members

   - Jasmin Christian Blanchette (VU Amsterdam, Netherlands -- co-chair)
   - Catalin Hritcu (Inria Paris, France -- co-chair)
   - Nada Amin (Harvard University - USA)
   - Jesús María Aransay Azofra (Universidad de La Rioja - Spain)
   - Mauricio Ayala-Rincon (Universidade de Brasilia - Brazil)
   - Liron Cohen (Cornell University - USA)
   - Dominique Devriese (Vrije Universiteit Brussel - Belgium)
   - Jean-Christophe Filliâtre (CNRS - France)
   - Adam Grabowski (University of Bialystok - Poland)
   - Warren Hunt (University of Texas - USA)
   - Ori Lahav (Tel Aviv University - Israel)
   - Peter Lammich (The University of Manchester - UK)
   - Dominique Larchey-Wendling (Univ. de Lorraine, CNRS, LORIA - France)
   - Hongjin Liang (Nanjing University - China)
   - Assia Mahboubi (Inria and VU Amsterdam - France)
   - Cesar Munoz (NASA - USA)
   - Vivek Nigam (fortiss GmbH - Germany)
   - Benjamin Pierce (University of Pennsylvania - USA)
   - Vincent Rahli (University of Luxembourg, SnT - Luxembourg)
   - Christine Rizkallah (UNSW Sydney - Australia)
   - Ilya Sergey (Yale-NUS College and National University of Singapore)
   - Kathrin Stark (Saarland University - Germany)
   - Nikhil Swamy (Microsoft Research - USA)
   - Nicolas Tabareau (Inria - France)
   - Dmitriy Traytel (ETH Zürich - Switzerland)
   - Floris van Doorn (University of Pittsburgh - USA)
   - Akihisa Yamada (National Institute of Informatics - Japan)
   - Roberto Zunino (University of Trento - Italy)

### Submission Guidelines

Prior to the paper submission deadline, the authors should upload their
**anonymized** paper in PDF format through the HotCRP system at

Re: [fstar-club] INSTALL.md

[Catalin Hritcu via fstar-club]

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-from-sources,
> paragraph "Instructions for all OSes", Step 4, in the line
> $ opam install ocamlbuild ocamlfind ...,
> the 'pprint' package is listed twice. Maybe this is wanted?
>
> Best regards,
> Paul Zimmermann
> ___
> fstar-club mailing list
> fstar-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club

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

[Catalin Hritcu via fstar-club]

---
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, 2019, Belval, Luxembourg

The summer school on verification technology, systems & applications
focuses on fundamental aspects of verification techniques, their
implementation, and their use for concrete applications. It is organized by
Inria Nancy, the Max-Planck-Institut für Informatik in Saarbrücken, and the
Universities of Liège and of Luxembourg, and will take place at the
University of Luxembourg, Belval Campus, Maison du Savoir from July 1 to 5,
2019.


The following speakers have agreed to lecture at the school:

- Alexey Gotsman: Reasoning about data consistency in distributed systems
- Jochen Hoenicke: Software model checking with Ultimate
- Catalin Hritcu: Program verification with F*
- Marieke Huisman: Verification of concurrent and distributed software
- Cezary Kaliszyk: Artificial intelligence in theorem proving

Participation in the school is free to anybody holding at least a bachelor
degree or equivalent; it includes the lectures, coffee and lunch breaks,
and a school dinner. Attendance is limited to 40 participants. Please apply
electronically by sending an email to Soumya Paul (soumya.p...@uni.lu)
including

- a one-page CV,
- an application letter explaining your interest in the school and your
experience in the area
- a copy of your bachelor certificate (or equivalent or a more significant
certificate)
- a short statement if you want to contribute to the student sessions

Full details can be found on the school Web page at
https://www.mpi-inf.mpg.de/vtsa19
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club

Re: [fstar-club] FStar school

[Catalin Hritcu via fstar-club]

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, Systems, and Applications,
Luxembourg
- Application deadline: 10 May, School: 1-5 July

Cheers,
Catalin

On Tue, Apr 2, 2019 at 9:46 PM Marc Gourjon via fstar-club
 wrote:
>
> Dear FStar-experts,
> will there be another occasion to learn Fstar interactively with you?
> Something like the EUTypes meeting in Aarhus last year.
>
> An in-depth session would be really beneficial (at least to me), despite
> the good amount of papers, tutorials, wiki and zulip assistance!
> Maybe Tactics benefit from some special treatment as well ;)
>
> KR
> Marc
>
> --
> Marc Gourjon
> Security in Distributed Applications
> Hamburg University of Technology (TUHH)
> http://www.tuhh.de/sva
> ___
> fstar-club mailing list
> fstar-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club

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

[Catalin Hritcu via fstar-club]

**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 of some sort, preferably
with the production of independently checkable certificates.
CPP spans areas of computer science, mathematics, logics, and education.

CPP 2020 will be held on 20-21 January 2020 in New Orleans, Louisiana,
United States and will be co-located with POPL 2020. CPP 2020 is
sponsored by ACM SIGPLAN, in cooperation with ACM SIGLOG.

For more information about this edition and the CPP series please visit:
https://popl20.sigplan.org/home/CPP-2020

### Important Dates

   - Abstract Deadline: 16 October 2019 at 23:59 AoE (UTC-12h)
   - Paper Submission Deadline: 21 October 2019 at 23:59 AoE (UTC-12h)
   - Conference: 20 - 21 January 2020

### Topics of Interest

We welcome submissions in research areas related to formal
certification of programs and proofs. The following is a
non-exhaustive list of topics of interests to CPP:

   - certified or certifying programming, compilation, linking, OS
 kernels, runtime systems, and security monitors;
   - certified mathematical libraries and mathematical theorems;
   - proof assistants (e.g, ACL2, Agda, Coq, Dafny, F*, HOL,
 HOL-Light, Idris, Isabelle, Lean, Mizar, Nuprl, PVS, etc)
   - new languages and tools for certified programming;
   - program analysis, program verification, and program synthesis;
   - program logics, type systems, and semantics for certified code;
   - logics for certifying concurrent and distributed systems;
   - mechanized metatheory, formalized programming language semantics,
 and logical frameworks;
   - higher-order logics, dependent type theory, proof theory,
 logical systems, separation logics, and logics for security;
   - verification of correctness and security properties;
   - formally verified blockchains and smart contracts;
   - certificates for decision procedures, including linear algebra,
 polynomial systems, SAT, SMT, and unification in algebras of interest;
   - certificates for semi-decision procedures, including equality,
 first-order logic, and higher-order unification;
   - certificates for program termination;
   - formal models of computation;
   - mechanized (un)decidability and computational complexity proofs;
   - user interfaces for proof assistants and theorem provers
   - teaching mathematics and computer science with proof assistants.

### Program Committee Members

   - Nada Amin (Harvard University - USA)
   - Jesús María Aransay Azofra (Universidad de La Rioja - Spain)
   - Mauricio Ayala-Rincon (Universidade de Brasilia - Brazil)
   - Liron Cohen (Cornell University - USA)
   - Dominique Devriese (Vrije Universiteit Brussel - Belgium)
   - Jean-Christophe Filliâtre (CNRS - France)
   - Adam Grabowski (University of Bialystok - Poland)
   - Warren Hunt (University of Texas - USA)
   - Ori Lahav (Tel Aviv University - Israel)
   - Peter Lammich (The University of Manchester - UK)
   - Dominique Larchey-Wendling (Univ. de Lorraine, CNRS, LORIA - France)
   - Hongjin Liang (Nanjing University - China)
   - Assia Mahboubi (Inria and VU Amsterdam - France)
   - Cesar Munoz (NASA - USA)
   - Vivek Nigam (fortiss GmbH - Germany)
   - Benjamin Pierce (University of Pennsylvania - USA)
   - Vincent Rahli (University of Luxembourg, SnT - Luxembourg)
   - Christine Rizkallah (UNSW Sydney - Australia)
   - Ilya Sergey (Yale-NUS College and National University of Singapore)
   - Kathrin Stark (Saarland University - Germany)
   - Nikhil Swamy (Microsoft Research - USA)
   - Nicolas Tabareau (Inria - France)
   - Dmitriy Traytel (ETH Zürich - Switzerland)
   - Floris van Doorn (University of Pittsburgh - USA)
   - Akihisa Yamada (National Institute of Informatics - Japan)
   - Roberto Zunino (University of Trento - Italy)

### Submission Guidelines

Submission guidelines will be made available in due course.

### Contact

For any questions please contact the two PC chairs:
Jasmin Christian Blanchette ,
Catalin Hritcu 
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club

[fstar-club] F* v0.9.6.0 released

[Catalin Hritcu via fstar-club]

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
this [report](https://arxiv.org/abs/1803.06547). Code samples are in
examples/tactics, examples/native_tactics and the `FStar.Tactics` and
`FStar.Reflection` libraries. Many people contributed a lot to this
work, especially Guido Martinez.

- Improved type inference with two-phase typechecking: We now build
verification conditions for a program after a first phase of type
inference. This improves inference of implicit arguments and reduces
our trust in the type inference. Thanks to Aseem Rastogi!

- Caching typechecked modules: F* emits ".checked" files, an on-disk
representation of a typechecked module that can be read back later.
This significantly reduces the time to load a module's dependences.

# Many other improvements

A sampling of improvements across the entire tool chain:

- Resolving several syntactic ambiguities in the parser

- A correct pretty printer for surface terms, using `fstar --indent`

- A new dependence analysis to support incremental compilation for
larger projects

- Overhauling the higher order unification algorithm, both in the
representation of meta-variables and in the handling of unfolding,
leading to significant performance and robustness improvements (see
https://github.com/FStarLang/FStar/wiki/Design-note:-Revising-the-unifier)

- Automatic generation of interfaces for modules and tighter
enforcement of abstraction boundaries (see
https://github.com/FStarLang/FStar/wiki/Revised-checking-of-a-module's-interface)

- Improvements to the SMT encoding, removing axioms that lead to
performance problems and reducing brittleness related to optimizations
in the encoding, notably shallow vs deep encodings

- Improved type-based erasure for extraction

- Several new and improved libraries, including a revised treatment of
footprints for Low* programs, in `FStar.Modifies`

- And work by many people in Project Everest whose use of F* drove a
lot of the work in this release.

- Plus many other improvements and changes as described in
https://github.com/FStarLang/FStar/blob/v0.9.6.0/CHANGES.md

- And 180 closed github issues
https://github.com/FStarLang/FStar/issues?q=is%3Aissue+is%3Aclosed+closed%3A%222017-08-23+..+2018-05-17%22
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club

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

[Catalin Hritcu via fstar-club]

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
*Objet :* [fmics] Two PhD offers at Inria, Rennes, on refinement types for
system design



Two competitive PhD offers are available with Inria project-team TEA at
Inria-Rennes - IRISA:



* "Type theory for modular static analysis of system programs", in
collaboration with project-team CELTIQUE

  Details: https://www.irisa.fr/fr/offres-theses/theorie-types-
lanalyse-statique-modulaire-programmes-systeme



* "Refinement types for stream-processing systems", in collaboration with
team VAADER at IETR, Rennes.

  Details: https://www.irisa.fr/fr/offres-theses/typage-
raffinement-systemes-traitement-du-signal



Jean-Pierre Talpin
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club

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

[Catalin Hritcu via fstar-club]

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 paper
   )
   - A revision of the libraries based on a new formal account of monotonic
   state (see this paper )
   - Extraction of programs with user-defined effects
   - Experimental support for tactics
   - New IDE protocol
    and new
   IDE features :
   autocompletion, evaluation, real-time syntax checking, jump-to-definition,
   type-at-point, etc.

Changes and other improvements

   - A reorganization of the library and a single fstarlib.cmxa against
   which to link all F* programs compiled to OCaml (this change is
   incompatible with previous versions of F*)
   - A new printer of source terms
   - Revised error reporting from failed SMT queries
   - Improved support for separate compilation via a binary format for
   checked modules
   - Fixed a ton of bugs (179 closed GitHub issues
   

   )
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club

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

[Catalin Hritcu via fstar-club]

>> 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-fuel-and-the-normalizer#using-the-f-normalizer


>> On Mon, May 15, 2017 at 4:03 PM, Catalin Hritcu
>>  wrote:
>>> 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 for the unfolding lemma to be unprovable?

 Thanks!
 Clément.

 module Scratch

 open FStar.List

 assume val pairs_with_sum (n: nat) : list (p: (nat * nat){fst p + snd 
 p == n})

 assume val product (#a #b: Type) (l1: list a) (l2: list b) : list (a * 
 b)

 type bin_tree =
 | Leaf
 | Branch of bin_tree * bin_tree

 let rec size bt : nat =
   match bt with
   | Leaf -> 0
   | Branch(l, r) -> 1 + size l + size r

 let rec trees_of_size (s: nat) : list bin_tree =
   if s = 0 then
 [Leaf]
   else
 List.Tot.concatMap #(p: (nat * nat){(fst p) + (snd p) == s - 1})
   (fun (s1, s2) -> List.Tot.map Branch (product (trees_of_size s1) 
 (trees_of_size s2)))
   (pairs_with_sum (s - 1))

 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 
 - 1})
  (fun (s1, s2) -> List.Tot.map Branch (product 
 (trees_of_size s1) (trees_of_size s2)))
  (pairs_with_sum (s - 1 = ()
 ___
 fstar-club mailing list
 fstar-club@lists.gforge.inria.fr
 https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
>>
>
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club

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

[Catalin Hritcu via fstar-club]

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

PhD - Refinement types for stream processing languages
https://www.inria.fr/en/centre/rennes/overview/offers/phd/campaign-2017/(view)/details.html?id=PNGFK026203F3VBQB6G68LOE1=4509=7840=EN=10=11169=17755=52=DESC=28

PhD - Refinement types for cyber-physical system design
https://www.irisa.fr/fr/offres-theses/refinement-types-cyber-physical-system-design

PostDoc - From liquid types to certified code (deadline passed)
https://www.inria.fr/en/institute/recruitment/offers/post-doctoral-research-fellowships/post-doctoral-research-fellowships/(view)/details.html?id=PNGFK026203F3VBQB6G68LOE1=4508=EN=20=11122=17707=52=DESC=19
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club