Lucas Franceschino

icon indicating a website link http://lucas.franceschino.fr icon indicating an email [email protected]

icon company Cryspen icon location France icon location Research Engineer at @cryspen

Results 275 comments of Lucas Franceschino

F*: interface mode: missed binders

This is still relevant. This transformation should be done outside of the backend, as a phase.

F*: interface mode: missed binders

✅

Make sure const generics/types/impls are correctly transported everywhere in the engine

Still relevant

Make sure const generics/types/impls are correctly transported everywhere in the engine

This is still relevant, but we will probably just enforce that while slowly migrating phases from OCaml to Rust. Thus I'm closing.

Engine: uniformize `ty` VS `typ`

Still relevant

Engine: uniformize `ty` VS `typ`

Not planned: we will deprecate the OCaml engine

Equality constraints meta issue

Still relevant

Equality constraints meta issue

Still an issue

Make Rust code executable via F* extraction

This is in progress with the new annotated core library, thus still relevant.

Engine: refactor `place_to_lhs`s, make informal invariant into type system

Still relevant