Alessio Coltellacci

Après Docker, les Unikernels ?

2

Language of the talk: - [x] 🇫🇷 - [ ] 🇬🇧 ## About you * Name: Coltellacci Alessio * Link to profile picture (best quality you have): * Job title:...

Fail to establish physical links to external symbols

4

Hi ! I am working on a way to split my long proof into multiple files to check them across multiprocess. Each proof is cut into a segment that contains...

I have investigated the reconstruction of arithmetic proofs from Alethe. For now, I want to try to reconstruct only the steps that provide the coefficients for the simplex. Example: Here...

Problem with eval tactic

2

I propose to open this issue to track the progress of the new eval tactic introduced in #1202. The pull request proposed these changes: - [x] find a way to...

The modifier associative commutative can be slow with large terms

1

Hi everyone, I am trying to use the modifier `associative commutative` to run reflective proof similar to `lia` and `lia` from Coq. I would like to use the `associative commutative`...

Rewriting rules do not compute correctly on term defined by a `set` tactic ?

12

Hi everyone, I am facing a strange behavior that I tried to summarize in this [gist](https://gist.github.com/NotBad4U/13073244d5ab7c9293890477b864ca15). I am using the `set` tactic in my generated proof to make the reconstruction...

Hi everyone, I hit a performance issue in the Lambdapi kernel when using rewrite on a reflective proof of contraction for propositional disjunctions. Even on a very small example, the...