Difference between revisions of "Formal system"
From apm
m |
(→External links: dependent types) |
||
| Line 17: | Line 17: | ||
* [https://en.wikipedia.org/wiki/Lambda_calculus Untyped_lambda_calculus], [https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus Simply_typed_lambda_calculus], [https://en.wikipedia.org/wiki/Typed_lambda_calculus Typed_lambda_calculus], [https://en.wikipedia.org/wiki/System_F System_F] | * [https://en.wikipedia.org/wiki/Lambda_calculus Untyped_lambda_calculus], [https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus Simply_typed_lambda_calculus], [https://en.wikipedia.org/wiki/Typed_lambda_calculus Typed_lambda_calculus], [https://en.wikipedia.org/wiki/System_F System_F] | ||
* [https://en.wikipedia.org/wiki/Evaluation_strategy Evaluation_strategy], [https://en.wikipedia.org/wiki/De_Bruijn_index De_Bruijn_index] (or better [https://pchiusano.github.io/2014-06-20/simple-debruijn-alternative.html alternative]) | * [https://en.wikipedia.org/wiki/Evaluation_strategy Evaluation_strategy], [https://en.wikipedia.org/wiki/De_Bruijn_index De_Bruijn_index] (or better [https://pchiusano.github.io/2014-06-20/simple-debruijn-alternative.html alternative]) | ||
| − | * [https://en.wikipedia.org/wiki/Lambda_cube Lambda_cube] | + | * [https://en.wikipedia.org/wiki/Lambda_cube Lambda_cube], [https://en.wikipedia.org/wiki/Dependent_type Dependent_type] |
---- | ---- | ||
* [https://en.wikipedia.org/wiki/Foundations_of_mathematics Foundations_of_mathematics], [https://en.wikipedia.org/wiki/Category_theory Category_theory], [https://en.wikipedia.org/wiki/Corecursion Corecursion] | * [https://en.wikipedia.org/wiki/Foundations_of_mathematics Foundations_of_mathematics], [https://en.wikipedia.org/wiki/Category_theory Category_theory], [https://en.wikipedia.org/wiki/Corecursion Corecursion] | ||
Revision as of 11:43, 16 July 2017
External links
- Experiencing systems as a puzzle game - very good! http://incredible.pm/
Wikipedia
- Formal_system, Formal_language, Formal_grammar (Abstract_syntax_tree, Backus–Naur_form)
- Rewriting and Substitution, Explicit_substitution
- Chomsky_hierarchy
- Boolean_algebra (De Morgan's laws, Karnaugh_map)
- Propositional_calculus, Second-order_propositional_logic (Second-order_logic), Higher-order_logic
- Intuitionistic_logic, Intuitionistic_type_theory, Curry–Howard_correspondence
- Untyped_lambda_calculus, Simply_typed_lambda_calculus, Typed_lambda_calculus, System_F
- Evaluation_strategy, De_Bruijn_index (or better alternative)
- Lambda_cube, Dependent_type
- Foundations_of_mathematics, Category_theory, Corecursion
- Categorical_logic Bicartesian_closed_category (Homotopy type theory, Lawvere theories)
