User loginNavigation 
Curry Howard and more powerful type systemsThe ongoing thread On the (Alleged) Value of Proof for Assurance has sparked a discussion about applying the Curry Howard Isomorphism to more than intuitionistic logic and the simply typed LC. All these attempts are rather handwavey to me, but the discussion revolves around Isabelle and Coq, neither of which do I know. Neelk has made it pretty clear that CH does not apply to Isabelle, but it has gotten me wondering. * Is there a rigorous way to apply CH to a more powerful type system than the simply typed LC? * Is it nonsensical to try and apply it? * Does the ability to typecheck nonterminating expressions have an impact? Similarly, do existential types? (I'm thinking FOmega) * Are there any articles/books that do apply it to more powerful type systems which are accessible to someone without a PhD? By Brandon Niemczyk at 20100323 01:43  LtU Forum  previous forum topic  next forum topic  other blogs  3766 reads

Browse archivesActive forum topics 
Recent comments
1 day 3 hours ago
1 day 8 hours ago
2 days 8 hours ago
2 days 10 hours ago
2 days 16 hours ago
3 days 9 hours ago
3 days 18 hours ago
4 days 5 hours ago
4 days 6 hours ago
4 days 6 hours ago