2 papers
cs.LO2026
Justification Logic of the Lambda Calculus
Silvia Ghilezan, Paaras Padhiar
The simply typed λ-calculus is a model of computation where typed terms correspond to proofs of intuitionistic propositional logic (IPL) via the Curry-Howard correspondence. Justi…
cs.LO2026
List types for resource aware languages: an implicit name approach
Silvia Ghilezan, Jelena IvetiÄ, Pierre Lescanne +1
A novel formalisation of variable control in languages with implicit names based on de Bruijn indices is presented. We design and implement three languages: first, a restricted lan…