Thiago Felicissimo

Type inference with implicit arguments

2

In some cases, it is possible to use implicit arguments to build a term which can be elaborated into different terms having different types (modulo =_R). It seems that, when...

Taking types into account when checking local confluence is not sound

2

This is a counterexample to the technique of taking typability constraints into account when checking local confluence. This technique apparently had been implemented by [this PR](https://github.com/Deducteam/lambdapi/pull/837) but I had seen...

Exports for the format TRS + small improvement to HRS export

5

This provides an export for the TRS format used by checkers such as Aprove. It can be used to check SN without beta, and only works for rewrite systems that...

Printing of metavariable names

5

There used to be a time in which, when lambdapi failed to verify that a rule preserves typing, the error message would show the metavariables with their actual names in...