커리-하워드 대응
논리학에서 커리-하워드 대응(Curry-Howard correspondence) 또는 커리-하워드 동형(Curry-Howard isomorphism)은 컴퓨터 프로그램과 논리적 증명을 직접적으로 연관시키는 대응 관계이다. 하스켈 커리와 윌리엄 앨빈 하워드(William Alvin Howard)에 의해 소개된 개념이다.
정확히 말하면 커리-하워드 대응은 논리의 증명 연산(proof calculus)과 컴퓨터의 형 체계(type system)가 대응된다는 진술이다. 예를 들어 힐베르트 체계(Hilbert system)와 콤비네이터 논리(combinatory logic)가, 자연 연역과 람다 계산이 대응된다.
본래 컴퓨터는 구성적인 과정만을 수행가능하기 때문에 증명이 온전히 구성적인 직관 논리에 있어서만 성립하는 것으로서 여겨졌으나 최근에 들어서는 고전 논리에서만 성립하는 비구성적인 개념들은 continuation과 대응됨이 알려졌다.