News for hackers. Stuff that matters.

A comment on The λ-Cube. Parent comment

Re:The λ-Cube by creata on Saturday January 15, 2022 @11:29PM (#29953333)
> a proof development system, aka dependently typed programming language.

There are proof assistants without dependent types, like Isabelle/HOL.

[ Parent | on HN ]

There are no comments on this comment yet.