William Alvin Howard zauważył, że system dowodowy „wysokiego poziomu”, zwany dedukcją naturalną, można bezpośrednio interpretować w jego intuicyjnej wersji jako typowy wariant modelu obliczeniowego zwanego rachunkiem lambda. To stało się znane jako izomorfizm Curry’ego-Howarda.
Lata 70. XX w. W 1970 r. Dana Scott opublikował pracę na temat semantyki denotacyjnej. W 1972 r. opracowano programowanie logiczne i Prolog, umożliwiając tym samym wyrażanie programów komputerowych jako logiki matematycznej. Zespół naukowców z Xerox PARC, kierowany przez Alana Kaya, opracował Smalltalk, język obiektowy znany z innowacyjnego środowiska programistycznego. W 1974 r. John C. Reynolds odkrył System F, który jak się okazało został odkryty niezależnie 3 lata wcześnniej przez logika Jean-Yves Girarda. Od 1975 r. Gerald Jay Sussman i Guy Steele opracowują język programowania Scheme, dialekt Lisp obejmujący zasięg leksykalny, ujednoliconą przestrzeń nazw oraz elementy z modelu aktorskiego (ang. actor model), w tym kontynuacje (ang. continuation) pierwszej klasy. Backus podczas wykładu ACM Turing Award w 1977 r. skrytykował stan języków przemysłowych i zaproponował nową klasę języków programowania, znaną obecnie jako języki programowania na poziomie funkcji (ang. function-level programming). W 1977 r.