프로그래밍 언어 이론

섬네일|250px|소문자 그리스 문자 λ(람다)는 프로그래밍 언어 이론 분야의 비공식적인 상징이다. 이 용법은 1930년대 알론조 처치가 도입하고 프로그래밍 언어 연구자들이 널리 사용하는 계산 모델인 람다 대수에서 유래한다. 이는 고전적인 텍스트인 Structure and Interpretation of Computer Programs의 표지를 장식하고 있으며, 스킴 언어 개발자인 제럴드 제이 서스먼과 가이 L. 스틸 주니어가 쓴 1975년부터 1980년까지의 소위 Lambda Papers의 제목이기도 하다.

프로그래밍 언어 이론(Programming language theory, PLT)은 프로그래밍 언어로 알려진 형식 언어의 설계, 구현, 분석, 특성화 및 분류를 다루는 컴퓨터 과학의 한 분야이다. 프로그래밍 언어 이론은 언어학, 수학, 소프트웨어 공학을 포함한 다른 분야와 밀접한 관련이 있다.

 역사 

어떤 면에서 프로그래밍 언어 이론의 역사는 프로그래밍 언어 개발보다 앞선다. 1930년대 알론조 처치와 스티븐 클레이니가 개발한 람다 대수는 프로그래머가 컴퓨터 시스템에 알고리즘을 설명하는 수단이라기보다는 계산을 모델링하기 위한 것이었지만, 일부에서는 이를 세계 최초의 프로그래밍 언어로 간주한다. 많은 현대 함수형 프로그래밍 언어는 람다 대수 위에 "얇은 베니어판"을 제공하는 것으로 묘사되었으며, 많은 언어가 람다 대수 관점에서 쉽게 설명된다.

최초로 발명된 프로그래밍 언어는 1940년대 콘라트 추제가 설계한 플랑칼퀼이지만, 1972년까지 대중에게 알려지지 않았고 1998년까지 구현되지 않았다. 최초로 널리 알려지고 성공한 고급 프로그래밍 언어는 1954년부터 1957년까지 존 배커스가 이끄는 IBM 연구팀이 개발한 FORTRAN (Formula Translation)이었다. FORTRAN의 성공으로 과학자 위원회가 "보편적인" 컴퓨터 언어를 개발하기 위해 구성되었으며, 그 노력의 결과가 ALGOL 58이었다. 별도로 매사추세츠 공과대학교(MIT)의 존 매카시는 학계에서 성공을 거둔 최초의 언어인 리습을 개발했다. 이러한 초기 노력의 성공으로 프로그래밍 언어는 1960년대 이후 활발한 연구 주제가 되었다.

 연표 

그 이후 프로그래밍 언어 이론 역사에서 몇 가지 주요 사건들:

 1950년대
 노엄 촘스키는 언어학 분야에서 촘스키 위계를 개발했는데, 이는 프로그래밍 언어 이론 및 기타 컴퓨터 과학 분야에 직접적인 영향을 미쳤다.

 1960년대
 1962년, 올레요한 달과 크리스텐 니고르가 시뮬라 언어를 개발했다. 시뮬라는 객체 지향 프로그래밍 언어의 첫 번째 예시로 널리 간주되며, 코루틴 개념도 도입했다.
 1964년, 피터 랜딘은 처치의 람다 대수가 프로그래밍 언어를 모델링하는 데 사용될 수 있음을 처음으로 깨달았다. 그는 람다 표현식을 "해석"하는 SECD 머신을 소개했다.
 1965년, 랜딘은 본질적으로 연속의 한 형태인 J 연산자를 소개했다.
 1966년, 랜딘은 그의 논문 "다음 700가지 프로그래밍 언어"에서 추상적인 컴퓨터 프로그래밍 언어인 ISWIM을 소개했다. 이는 하스켈 언어로 이어지는 언어 설계에 영향을 미쳤다.
 1966년, 코라도 뵘은 CUCH(Curry-Church) 언어를 소개했다.
 1967년, 크리스토퍼 스트래치는 그의 영향력 있는 강의 노트 Fundamental Concepts in Programming Languages를 발표하여 R값, L값, 매개변수 다형성, 애드혹 다형성이라는 용어를 도입했다.
 1969년, J. 로저 힌들리는 조합 논리에서 객체의 주 유형 스킴을 발표했으며, 이는 나중에 힌들리-밀너 유형 추론 알고리즘으로 일반화되었다.
 1969년, 토니 호어는 공리적 의미론의 한 형태인 호어 논리를 도입했다.
 1969년, 윌리엄 앨빈 하워드는 자연 연역이라고 불리는 "고수준" 증명 시스템이 그 직관주의적 버전에서 람다 대수로 알려진 계산 모델의 타입이 있는 변형으로 직접 해석될 수 있음을 관찰했다. 이는 커리-하워드 대응으로 알려지게 되었다.

 1970년대
 1970년, 데이나 스콧은 표시적 의미론에 대한 그의 연구를 처음 발표했다.
 1972년, 논리형 프로그래밍과 프롤로그가 개발되어 컴퓨터 프로그램을 수학적 논리로 표현할 수 있게 되었다.
 앨런 케이가 이끄는 제록스 PARC의 과학자 팀은 혁신적인 개발 환경으로 널리 알려진 스몰토크라는 객체 지향 언어를 개발했다.
 1974년, 존 C. 레이놀즈는 System F를 발견했다. 이는 이미 1971년에 수학 논리학자 장-이브 기라르에 의해 발견되었다.
 1975년부터 제럴드 제이 서스먼과 가이 스틸은 어휘적 유효범위, 통합된 이름공간, 그리고 일급 연속을 포함한 행위자 모델의 요소를 통합한 리스프 방언인 스킴 언어를 개발했다.
 배커스는 1977년 튜링상 강연에서 당시의 산업 언어 상태를 비난하고 현재 함수 수준 프로그래밍 언어로 알려진 새로운 종류의 프로그래밍 언어를 제안했다.
 1977년, 고든 플로트킨은 추상적인 유형 함수형 언어인 Programming Computable Functions를 소개했다.
 1978년, 로빈 밀너는 ML 언어를 위한 힌들리-밀너 유형 시스템 추론 알고리즘을 도입했다. 유형 이론은 프로그래밍 언어에 대한 학문으로 적용되었고, 이러한 적용은 수년간 유형 이론의 큰 발전을 가져왔다.

 1980년대
 1981년, 고든 플로트킨은 구조적 동작 의미론에 대한 논문을 발표했다.
 1988년, 질 칸은 자연적 의미론에 대한 논문을 발표했다.
 로빈 밀너의 통신 시스템의 계산과 토니 호어의 커뮤니케이팅 시퀜셜 프로세스 모델, 그리고 칼 휴이트의 행위자 모델과 같은 유사한 동시성 모델과 같은 프로세스 계산이 등장했다.
 1985년, 미란다의 출시는 지연 평가되는 순수 함수형 프로그래밍 언어에 대한 학계의 관심을 불러일으켰다. 공개 표준을 정의하기 위한 위원회가 구성되어 1990년에 하스켈 1.0 표준이 발표되었다.
 베르트랑 메이어는 계약에 의한 설계 방법론을 만들고 이를 에펠 언어에 통합했다.

 1990년대
 그레고르 키찰레스, 짐 데스 리비에르 및 다니엘 G. 보브로는 The Art of the Metaobject Protocol 책을 출판했다.
 에우제니오 모기와 필립 와들러는 함수형 프로그래밍 언어로 작성된 프로그램을 구성하기 위해 모나드를 사용하는 방법을 도입했다.

 하위 분야 및 관련 분야 
프로그래밍 언어 이론 내에 있거나 이에 깊은 영향을 미치는 여러 연구 분야가 있으며, 이들 중 상당수는 상당한 중첩을 이룬다. 또한 PLT는 계산 가능성 이론, 범주론, 집합론을 포함한 많은 다른 수학 분야를 활용한다.

 형식 의미론 

형식 의미론은 컴퓨터 프로그램과 프로그래밍 언어의 동작에 대한 형식적인 명세이다. 컴퓨터 프로그램의 의미 또는 "의미"를 설명하는 세 가지 일반적인 접근 방식은 표시적 의미론, 동작적 의미론 및 공리적 의미론이다.

 유형 이론 

유형 이론은 자료형 체계에 대한 연구이며, 이는 "계산하는 값의 종류에 따라 구문을 분류하여 특정 프로그램 동작이 없음을 증명하는 다루기 쉬운 구문 방법"이다. 많은 프로그래밍 언어는 자료형 체계의 특성으로 구별된다.

 프로그램 분석 및 변환 

프로그램 분석은 프로그램을 검사하고 주요 특성(예: 특정 종류의 프로그램 오류 부재)을 결정하는 일반적인 문제이다. 프로그램 변환은 한 형식(언어)의 프로그램을 다른 형식으로 변환하는 과정이다.

 비교 프로그래밍 언어 분석 
비교 프로그래밍 언어 분석은 언어의 특성에 따라 언어를 다른 유형으로 분류하려고 한다. 넓은 범주의 언어는 종종 프로그래밍 패러다임으로 알려져 있다.

 제네릭 및 메타프로그래밍 
메타프로그래밍은 실행될 때 프로그램(다른 언어로 또는 원본 언어의 하위 집합으로)을 결과로 생성하는 고차원 프로그램의 생성이다.

 도메인 특화 언어 
도메인 특화 언어는 주어진 도메인 또는 해당 부분의 문제를 효율적으로 해결하기 위해 구성된 언어이다.

 컴파일러 구성 

컴파일러 이론은 컴파일러(또는 더 일반적으로 번역기)를 작성하는 이론이다. 즉, 한 언어로 작성된 프로그램을 다른 형식으로 번역하는 프로그램이다. 컴파일러의 동작은 전통적으로 구문 분석(스캔 및 구문 분석), 의미 분석(프로그램이 무엇을 해야 하는지 결정), 최적화(일부 측정 기준에 따라 프로그램의 성능 향상; 일반적으로 실행 속도) 및 코드 생성(일부 대상 언어로 동등한 프로그램 생성 및 출력; 종종 중앙 처리 장치(CPU)의 명령어 집합)으로 나뉜다.

 런타임 시스템 
런타임 시스템은 가상 머신, 쓰레기 수집 및 외부 함수 인터페이스를 포함한 프로그래밍 언어 런타임 환경과 그 구성 요소의 개발을 의미한다.

 학술지, 출판물 및 학회 
학회는 프로그래밍 언어 연구를 발표하는 주요 장소이다. 가장 잘 알려진 학회로는 프로그래밍 언어 원리 심포지엄(POPL), 프로그래밍 언어 설계 및 구현(PLDI), 국제 함수형 프로그래밍 학회(ICFP), 객체 지향 프로그래밍, 시스템, 언어 및 응용에 대한 국제 학회(OOPSLA) 및 ASPLOS가 있다.

PLT 연구를 게재하는 주목할 만한 학술지로는 ACM Transactions on Programming Languages and Systems(TOPLAS), Journal of Functional Programming(JFP), Journal of Functional and Logic Programming 및 Higher-Order and Symbolic Computation이 있다.

 같이 보기 
 SIGPLAN

 각주 

 추가 자료 
 아바디, 마르틴 및 카르델리, 루카. A Theory of Objects. Springer-Verlag.
 마이클 J. C. 고든. Programming Language Theory and Its Implementation. Prentice Hall.
 군터, 칼 및 미첼, 존 C. (편집). Theoretical Aspects of Object Oriented Programming Languages: Types, Semantics, and Language Design. MIT Press.
 하퍼, 로버트. Practical Foundations for Programming Languages. 초안.
 커누스, 도널드 E. (2003). Selected Papers on Computer Languages. 스탠포드, 캘리포니아: 언어 및 정보 연구 센터.
 미첼, 존 C. Foundations for Programming Languages.
 미첼, 존 C. Introduction to Programming Language Theory.
 오헌, 피터. W. 및 테넌트, 로버트. D. (1997). ALGOL-like Languages. Progress in Theoretical Computer Science. 비르크하우저, 보스턴.
 피어스, 벤자민 C. (2002). Types and Programming Languages. MIT Press.
 피어스, 벤자민 C. Advanced Topics in Types and Programming Languages.
 피어스, 벤자민 C. 외 (2010). Software Foundations.

 외부 링크 

 Lambda the Ultimate, 프로그래밍 언어 이론에 대한 전문적인 토론 및 문서 저장소를 위한 커뮤니티 웹로그.
 Great Works in Programming Languages. 벤자민 C. 피어스 (펜실베이니아 대학교) 수집.
 Classic Papers in Programming Languages and Logic. 칼 크레이리 (카네기 멜런 대학교) 수집.
 Programming Language Research. 마크 레오네 디렉터리.
 λ-Calculus: Then & Now 데이나 S. 스콧의 ACM 튜링 백주년 기념.
 Grand Challenges in Programming Languages. POPL 2009 패널 세션.