3 ms·
Plenty of advances in logic and category theory have enabled dependently typed languages to be both theorem prover and practical implementation language. See L
by agentultra 9y ago
Plenty of advances in logic and category theory have enabled dependently typed languages to be both theorem prover and practical implementation language.
See Lean.
- vladf 9y agoI'm interested but "Lean programming languages" and its varieties are difficult to Google. Would you mind posting a complete reference?
- cf 9y agoI think this is a good application paper for Lean showing how you can use it to develop machine learning algorithms. https://arxiv.org/abs/1706.08605 https://arxiv.org/abs/1706.08605
- agentultra 9y agoSorry I forgot the link! https://leanprover.github.io/ https://leanprover.github.io/