#nuprl — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #nuprl, aggregated by home.social.
-
Today, everyone in #IT fancies himself a connoisseur of dependent types. But David MacQueen—a pillar in the ML #FP community and the designer of the ML module system—was already leading the way in this area four decades ago. His 1986 paper, “Using Dependent Types to Express Modular Structure”, was the first time I came across the term #DependentTypes.
I did not have the knowledge and the perspective to fully appreciate the significance of MacQueen work, back then. Nor was I aware of Constable’s #NuPRL and similar proof assistants exploiting dependent types, in those days.
-
Today, everyone in #IT fancies himself a connoisseur of dependent types. But David MacQueen—a pillar in the ML #FP community and the designer of the ML module system—was already leading the way in this area four decades ago. His 1986 paper, “Using Dependent Types to Express Modular Structure”, was the first time I came across the term #DependentTypes.
I did not have the knowledge and the perspective to fully appreciate the significance of MacQueen work, back then. Nor was I aware of Constable’s #NuPRL and similar proof assistants exploiting dependent types, in those days.
-
It has been a while since I last time touched #nuprl but the way I think number theory proof is still affected by type theory
-
It has been a while since I last time touched #nuprl but the way I think number theory proof is still affected by type theory
-
Is #NuPRL dead? I'm a bit surprised that the latest update on https://nuprl.org/ is from 2016. More generally, is extensional type theory as a foundation for real practical programming languages and proof assistants dead?
-
Is #NuPRL dead? I'm a bit surprised that the latest update on https://nuprl.org/ is from 2016. More generally, is extensional type theory as a foundation for real practical programming languages and proof assistants dead?
-
Found people interested in #OpenGenera, anyone interested in #Nuprl or #MetaPRL, the dependent type theory theorem prover? One year before I have got MetaPRL working with recent version of OCaml, but did not have enough knowledge and time to continue the development.