Lambda Zoo Implemented: untyped simply-typed simply-typed with higher-kinded type operators (Weak Lambda Omega) system f system f omega lambda pi Useful links http://www.rbjones.com/rbjpub/logic/cl/tlc001.htm https://cstheory.stackexchange.com/a/36071