Formal system: Difference between revisions
Jump to navigation
Jump to search
→External links: dependent types |
formatting for better readability |
||
| (One intermediate revision by the same user not shown) | |||
| Line 3: | Line 3: | ||
== External links == | == External links == | ||
* Experiencing systems as a puzzle game - very good! http://incredible.pm/ | * Experiencing formal systems as a puzzle game - very good! <br> '''The Incredible Proof Machine http://incredible.pm/''' | ||
=== Wikipedia === | === Wikipedia === | ||
| Line 25: | Line 25: | ||
[[Category:Information]] | [[Category:Information]] | ||
[[Category:Programming]] | |||
Latest revision as of 10:50, 26 September 2021
External links
- Experiencing formal systems as a puzzle game - very good!
The Incredible Proof Machine 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)