Dependent Types + Combinatory Logic is highly non-trivial, as is shown in this series of work by Altenkirch et al.: https://drops.dagstuhl.de/entities/document

Dependent Types + Combinatory Logic is highly non-trivial, as is shown in this series of work by Altenkirch et al.: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.24 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.F... https://drops.dagstuhl.de/storage/00lipics/lipics-vol269-types2022/LIPIcs.TYPES.2022.10/LIPIcs.TYPES.2022.10.pdf https://drops.dagstuhl.de/storage/00lipics/lipics-vol269-typ... https://types2023.webs.upv.es/slides/S22/TYPES2023-Altenkirch-Kaposi-Sinkarovs-Vegh.pdf https://types2023.webs.upv.es/slides/S22/TYPES2023-Altenkirc... I wonder: Where does rholang3 fit in this?