A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction (Q1075050): Difference between revisions

We present a selection of articles dealing with constructive mathematics, from the point of view of the computer-aided synthesis of provably correct computer programs. Among the topics covered we find: typed \(\lambda\)-calculus, where types obey the Curry-Howard isomorphism between propositions and proofs; higher-order intuitionistic logic; computer- aided proof-checking and theorem-proving in type theory functional programming languages. There would be no point in attempting a complete bibliography of such an interdisciplinary area. Our aim is rather to provide the researcher with an up-to-date selection of work relevant to the current stream of research on de Bruijn's Automath languages, Girard's second-order types, and Martin-Löf's intuitionistic type theory.