운용 의미론

운영 의미론은 프로그램의 정확성, 안전성 또는 보안과 같은 특정 바람직한 특성이 수학적 의미를 용어에 부가하는 대신, 프로그램의 실행과 절차에 대한 논리적인 진술로부터 증명을 구성함으로써 검증되는 형식 프로그래밍 언어 의미론 범주입니다.운영 의미론은 두 가지 범주로 분류된다: 구조 운영 의미론(또는 작은 단계 의미론)은 컴퓨터 기반 시스템에서 계산의 개별 단계가 어떻게 일어나는지 공식적으로 기술한다; 반대 자연 의미론(또는 큰 단계 의미론)은 실행의 전체 결과가 어떻게 얻어지는지를 기술한다.프로그래밍 언어의 형식적 의미론을 제공하는 다른 접근법에는 자명한 의미론과 표현적 의미론이 포함된다.

프로그래밍 언어에 대한 운영 의미론은 유효한 프로그램이 계산 단계의 시퀀스로 어떻게 해석되는지를 기술합니다.이러한 시퀀스는 프로그램의 의미입니다.기능 프로그래밍의 맥락에서, 종료 시퀀스의 마지막 단계는 프로그램의 값을 반환합니다.(일반적으로 하나의 프로그램에는 많은 반환값이 있을 수 있다.왜냐하면 프로그램은 비결정론적일 수 있기 때문이다.그리고 결정론적 프로그램에도 시멘틱스가 그 값에 도달하는 연산의 시퀀스를 정확하게 규정하지 않을 수 있기 때문이다.)

아마도 연산 의미론의 첫 번째 형식적 화신은 ^[1]리스프의 의미론을 정의하기 위해 람다 미적분을 사용한 것일 것이다.SECD 머신의 전통에 따른 추상 머신도 밀접하게 관련되어 있습니다.

역사

연산 의미론의 개념은 알골 68의 의미론을 정의하는 데 처음으로 사용되었다.다음은 개정된 ALGOL 68 보고서의 인용문입니다.

엄밀한 언어로 된 프로그램의 의미는 그 프로그램의 상세 내용을 구성하는 일련의 동작을 수행하는 가상 컴퓨터의 관점에서 설명된다.(Algol68, 섹션 2)

현재의 의미에서의 "운영 의미론"이라는 용어의 첫 번째 사용은 Dana Scott(Plotkin04)에 기인한다.이어지는 것은 스콧의 공식 의미론에 대한 중요한 논문에서 인용한 것으로, 그는 의미론의 "작동적" 측면을 언급한다.

의미론에 대한 보다 '추상'과 '깨끗한' 접근법을 지향하는 것은 매우 좋지만, 계획이 조금이라도 좋다면, 운영 측면은 완전히 무시할 수 없다.(Scott70)

접근

Gordon Plotkin은 구조 운영 의미론, Matthias Felleisen과 Robert Hieb은 환원 ^[2]의미론, Gilles Kahn은 자연 의미론을 도입했다.

작은 단계의 의미론

구조 운영 의미론

구조적 운영 의미론(SOS, 구조화된 운영 의미론 또는 작은 단계 의미론이라고도 함)은 운영 의미론을 정의하기 위한 논리적 수단으로서 Gordon Plotkin 81)에 의해 도입되었다.SOS 뒤에 있는 기본 아이디어는 프로그램의 동작의 관점에서 프로그램의 동작을 정의함으로써 운영 의미론에 대한 구조적인, 즉 구문 지향적이고 귀납적인 관점을 제공하는 것입니다.SOS 사양은 (들)의 천이 관계의 관점에서 프로그램의 동작을 정의합니다.SOS 사양은 컴포넌트의 전환 측면에서 복합 구문의 유효한 전환을 정의하는 일련의 추론 규칙의 형태를 취합니다.

간단한 예시로, 우리는 단순한 프로그래밍 언어의 의미론의 일부를 고려한다. 적절한 예시는 Plotkin81과 Hennessy90 및 기타 교과서에 제시되어 있다. $C_{1},C_{2}$ 1, $C_{1},C_{2}$ 2({ $style$ C_ ${1}, C_{2})$ 를 $C_{1},C_{2}$ 언어의 프로그램 범위로 설정하고 $,$ s({ $displaystyle$ s})를 $s$ 상태 범위(예: 메모리 위치에서 값까지)로 $s$ 합니다.표현식( $E\displaystyle$ E $),$ $E$ 값 $($ \ $displaystyle$ V $V$ 및 위치( $\displaystyle$ L $)$ 가 있는 경우 메모리 업데이트명령어는 다음과 같은 의미를 가집니다.

$\displaystyle \frac E,s\rangle \오른쪽 화살표 V\langle L:=E,,,s\rangle \오른쪽 화살표 (s\mapsto V)}}}$

비공식적으로 규칙에는 " $s$ 의 $표현식$ E {\ $displaystyle$ E $}$ 가 $E$ $s$ $값$ V(\ $displaystyle$ V $V$ 로 감소하면 $L:=E$ L: $=$ L:= $E)$ 가 $L:=E$ $상태$ s {\ $displaystyle$ s $}$ 을 $s$ (를) $L=V$ L $(\displaystyle$ L $=V)$ 로 업데이트합니다."

시퀀스의 의미론은 다음 3가지 규칙으로 지정할 수 있습니다.

$(\displaystyle\frac\langle C_{1};C_{2},s\rangle \rongarrow C_{2},s\rangle C_{2}}}\quad \frac \langle C_{1},s\rongrangle C_1.},s\rangle \long rightrow s}}$

비공식적으로 첫 번째 규칙에서는 $s$ 의 $C_{1}$ $({$ $displaystyle$ $C_{1})$ 이 $C_{1}$ $s$ $상태$ $s$ s의프로그램 $C1$ ({ $displaystyle$ s $})$ 로 종료된 경우 $s$ 의 $C_{2}$ $C_{1};C_{2}$ ; $C_{1};C_{2}$ ; $C_{$ 1}; C_ ${$ 2}가 $C_{1};C_{2}$ 상태 $C_{2}$ 의 $프로그램$ C2({ $displaystyle$ i $})$ 로 축소됩니다.n state $s'$ . (You can think of this as formalizing "You can run $C_{1}$ , and then run $C_{2}$ using the resulting memory store.)두 번째 규칙에서는 $상태$ s의 $C_{1}$ $(\$ $displaystyle$ $C_{1})$ 이 $C_{1}$ $s'$ s의 $C_{1}'$ $(\$ $displaystyle$ $C_{1$ $s'$ 로 $C_{1}'$ 축소될 수 있는 $경우$ $상태$ s의 $C_{1};C_{2}$ ; $C_{1};C_{2}$ C2(\ $displaystyle$ $C_{1$ }; $C_2})$ 가 $C_{1};C_{2}$ $s$ 축소됩니다.o $C_{1}';C_{2}$ $C_{1}';C_{2}$ $C_{1}';C_{2}$ ; $C_{1}';C_{2}$ (\ $displaystyle$ $C_{1}$ ; $C_{2} in$ $state^{}$ s $s'$ ) 。 (이것은 최적화 컴파일러의 원칙을 공식화한 것으로 생각할 수 있습니다: " $C_{1}$ (\ $displaystyle C_{1}$ 은 $C_{1}$ 프로그램의 첫 번째 부분이라도 스탠드 얼론인 것처럼 $C_{1}$ 하는 것이 허용됩니다.cs는 구조적인 $C_{1};C_{2}$ 입니다.시퀀셜프로그램 $C_{1};C_{2}$ $(\$ 의 $C_{1}$ 는 $C_{1}$ C1(\ $displaystyle$ C_ ${$ 1 $C_{1}$ })의 $C_{2}$ 와 $C_{2}$ C2(\ $displaystyle C_{$ $2$ $C_{2}$ 의 의미에 의해 정의되기 때문입니다.

스테이트에 $B$ (\ $displaystyle$ B $B$ 로 이루어진 부울식도 있는 경우 ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$ while 명령어의 의미론을 정의할 수 ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$ , ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$ " " " " " " " " " " " s " t ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$ ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$ ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$ " w ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$ ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$ ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$ ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$ ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$ ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$ , ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$ " ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$ " " " " " " , " " " ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$ " " ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$ " " " ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$ " " " " " " " " " " " " " " ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$ " " " " " " " " " " " . " $le {\frac {\langle B,s\rangle \rightarrow \mathbf {true} {while} \ B \ \ \ mathbf {do } \ C , s \ longarrow \ langle C ; \ mathbf {while } \ B \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ mathbf { sangle }$

이러한 정의는 프로그램 동작의 공식적인 분석을 가능하게 하여 프로그램 간의 관계를 연구할 수 있게 한다.중요한 관계로는 시뮬레이션 사전 주문과 이중 시뮬레이션이 있다.이것들은 동시성 이론의 맥락에서 특히 유용하다.

직관적인 외관과 따라하기 쉬운 구조 덕분에 SOS는 큰 인기를 얻었으며 운영 의미론을 정의하는 데 있어 사실상의 표준이 되었습니다.성공의 신호로서, CiteSeer[1]에 따르면 SOS에 대한 원본 보고서(이른바 오르후스 보고서)는 1,000개 이상의 인용을 끌어모았으며, 컴퓨터 과학에서 가장 많이 인용된 기술 보고서 중 하나가 되었다.

환원 의미론

축소 의미론은 운영 의미론의 대체 표현입니다.그것의 핵심 아이디어는^[3] 1975년 고든 플롯킨에 의해 람다 미적분의 이름으로 순수한 함수 호출과 값 변형에 처음 적용되었고 1987년 그의 논문에서 마티아스 펠라이센에 의해 명령적 특징을 가진 고차 함수 언어에 일반화되었다.^[4]이 방법은 1992년 마티아스 펠라이슨과 로버트 히브에 의해 통제와 ^[2]국가를 위한 완전히 동등한 이론으로 더욱 상세하게 설명되었습니다."축소 의미론"이라는 문구 자체는 Felleisen과 Daniel Friedman에 의해 1987년 PARLE 논문에서 ^[5]처음 만들어졌다.

감소의미론은 각각 단일 잠재적 감소 단계를 지정하는 감소 규칙의 집합으로 제공됩니다.예를 들어, 다음 축소 규칙은 할당 문이 변수 선언 바로 옆에 있는 경우 축소할 수 있음을 나타냅니다.

$\displaystyle \mathbf {let\rec} \x=v_{1}\\mathbf {in} \x\왼쪽 화살표 v_{2};\ e\\ \ \ \ \ \ \ \ mathbf {let\ rec} \ x = v_{2} \ mathbf {in} \ e }$

할당문을 이러한 위치에 배치하기 위해 적절한 지점에 도달할 때까지 함수 어플리케이션과 할당문의 오른쪽을 통해 "버블업"됩니다. $\mathbf {let}$ t \ $displaystyle \mathbf {let}$ 표현식에 $\mathbf {let}$ 간섭하는 l $\mathbf {let}$ \ $displaystyle \mathbf {let}$ 표현식에 $\mathbf {let}$ $\mathbf {let}$ 압출 규칙도 필요합니다.대부분의 공개된 환원 의미론 용도는 평가 컨텍스트의 편의와 함께 이러한 "거품 규칙"을 정의합니다.예를 들어, 가치 언어에 의한 단순한 호출에서의 평가 컨텍스트의 문법은 다음과 같이 주어질 수 있습니다.

$\displaystyle E:=[,]\ v\ e\ x\ 왼쪽 화살표 E\\ mathbf {let\ rec} \ x = v \ mathbf { in } \ E \ \ \ \ big }\ e \$

$e$ 서e {\ $displaystyle$ e $}$ 는 $e$ 임의의 $v$ 을나타내고 v {\ $displaystyle$ v $}$ 는 $v$ 완전한 값을 나타냅니다.각 평가 컨텍스트에는 정확히 하나의 구멍[ $]$ \ $displaystyle$ [ , , $[\,]$ ]이 $[\,]$ 포함되어 있으며, 이 구멍에는 용어를 캡처하는 방법이 삽입되어 있습니다 $[\,]$ 콘텍스트의 모양은 이 구멍에서 감소가 발생할 수 있는 위치를 나타냅니다.평가 컨텍스트를 사용하여 "버블링"을 기술하려면 단일 공리로 충분합니다.

$\ displaystyle E [ , x \ left arrow v , \ e ] \ \ \ long rightrow \ x \ left arrow v ; \ E [ , e , ] \ qquad { ( 리프트 할당)}}}$

이 단일 감소 규칙은 과제 문장에 대한 Felleisen과 Hieb의 람다 미적분으로부터의 상승 규칙입니다.평가 컨텍스트에서는 이 규칙을 특정 용어로 제한하지만 람다를 포함한 모든 용어로 자유롭게 적용할 수 있습니다.

Plotkin에 이어 감소 규칙 집합에서 파생된 미적분의 유용성을 보여주는 것은 (1) 평가 함수를 유도하는 단일 단계 관계에 대한 처치-로저 보조 법칙과 (2) 비결정론적 탐색 i를 대체하는 단일 단계 관계에 대한 Curry-Fey 표준화 보조 법칙을 요구한다.n 결정론적 왼쪽 끝/가장 바깥쪽 검색을 사용한 평가 함수.Felleisen은 이 미적분의 명령적 확장이 이 이론들을 만족시킨다는 것을 보여주었다.이러한 정리들의 결과는 이 언어들의 타당한 추론 원칙인 대칭-추이-반사-폐쇄-등가 이론이 된다는 것이다.그러나 실제로 대부분의 환원 의미론 애플리케이션은 미적분을 사용하지 않고 표준 환원만을 사용한다(그리고 그것으로부터 도출할 수 있는 평가자).

감소 의미론은 평가 컨텍스트가 상태 또는 비정상적인 제어 구조(예: 1등급 연속)를 모델링할 수 있는 용이성을 고려할 때 특히 유용하다.또한 축소 의미론은 ^[6]객체 지향 언어, 계약 시스템, 예외, 미래, 필요에 따른 호출 및 기타 많은 언어 특징을 모델링하기 위해 사용되어 왔습니다.PLT Redex의 ^[7]시멘틱스 엔지니어링의 Matthias Felleisen, Robert Bruce Findler 및 Matthew Flatt에 의해 그러한 몇 가지 응용에 대해 상세히 논의되는 리덕션 시멘틱스의 철저하고 현대적인 처리가 제시되었다.

큰 단계의 의미론

자연 의미론

큰 단계 구조 운영 의미론은 자연 의미론, 관계 의미론 및 평가 ^[8]의미론이라는 이름으로도 알려져 있다.Gilles Kahn이 ML의 순수 방언인 Mini-ML을 제시할 때 자연 의미론이라는 이름으로 큰 단계 운영 의미론을 도입하였다.

큰 단계의 정의를 함수의 정의로 볼 수 있으며, 보다 일반적으로는 관계 정의로 볼 수 있으며, 적절한 영역의 각 언어 구조를 해석할 수 있습니다.직관성은 프로그래밍 언어에서 의미론 지정에 널리 사용되는 선택이지만 제어집약적 기능이나 동시성을 가진 언어 등 많은 상황에서 사용하기 불편하거나 불가능한 단점이 있습니다.

큰 스텝의 의미론은 언어구조의 최종평가결과를 구문상대(하위식, 부표현 등)의 평가결과를 조합함으로써 어떻게 얻을 수 있는지를 나눗셈 앤 정복 방식으로 기술한다.

비교

작은 단계와 큰 단계 의미론 사이에는 프로그래밍 언어의 의미론을 규정하는 데 어느 쪽이 더 적합한 기초를 형성하는지 여부에 영향을 미치는 많은 차이점이 있습니다.

큰 단계 의미론은 종종 더 단순하다는 장점이 있으며(추론 규칙이 더 적게 필요함), 종종 언어에 대한 통역자의 효율적인 구현에 직접적으로 대응한다(따라서 칸은 "자연적"이라고 부른다).둘 다 예를 들어 일부 프로그램 ^[9]변환에서 정확성 보존을 증명할 때 보다 간단한 증명으로 이어질 수 있습니다.

빅 스텝 의미론의 주요 단점은 비종단(분할) 계산에는 추론 트리가 없기 때문에 그러한 ^[9]계산에 대한 속성을 기술하고 증명할 수 없다는 것이다.

작은 단계의 의미론은 평가의 세부사항과 순서를 더 잘 제어할 수 있도록 합니다.계측된 운영 시멘틱스의 경우, 이는 운영 시멘틱스가 추적하고 의미론자가 언어의 런타임 동작에 대한 보다 정확한 이론을 진술하고 증명할 수 있도록 한다.이러한 속성은 작은 단계의 의미론을 보다 편리하게 하여 운영 ^[9]의미론에 대한 유형 시스템의 유형 건전성을 증명합니다.

「」를 참조해 주세요.

레퍼런스

^ McCarthy, John. "Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I". Archived from the original on 2013-10-04. Retrieved 2006-10-13.
^ ^a ^b Felleisen, M.; Hieb, R. (1992). "The Revised Report on the Syntactic Theories of Sequential Control and State". Theoretical Computer Science. 103 (2): 235–271. doi:10.1016/0304-3975(92)90014-7.
^ Plotkin, Gordon (1975). "Call-by-name, call-by-value and the λ-calculus" (PDF). Theoretical Computer Science. 1 (2): 125–159. doi:10.1016/0304-3975(75)90017-1. Retrieved July 22, 2021.
^ Felleisen, Matthias (1987). The calculi of Lambda-v-CS conversion: a syntactic theory of control and state in imperative higher-order programming languages (PDF) (PhD). Indiana University. Retrieved July 22, 2021.
^ Felleisen, Matthias; Friedman, Daniel P. (1987). "A Reduction Semantics for Imperative Higher-Order Languages". Proceedings of the Parallel Architectures and Languages Europe. International Conference on Parallel Architectures and Languages Europe. Vol. 1. Springer-Verlag. pp. 206–223. doi:10.1007/3-540-17945-3_12.
^ Abadi, M.; Cardelli, L. (8 September 2012). A Theory of Objects. ISBN 9781441985989.
^ Felleisen, Matthias; Findler, Robert Bruce; Flatt, Matthew (2009). Semantics Engineering with PLT Redex. The MIT Press. ISBN 978-0-262-06275-6.
^ 일리노이 대학교 CS422
^ ^a ^b ^c 자비에 르로이."유도적인 큰 단계 운영 의미론"

추가 정보

길레스 칸"자연 의미론"제4회 컴퓨터 사이언스의 이론적 측면에 관한 심포지엄의 진행.스프링거-벨라그.1987년 런던
Gordon D. Plotkin. A Structural Approach to Operational Semantics. (1981) Tech. Rep. DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark. (Reprinted with corrections in J. Log. Algebr. Program. 60-61: 17-139 (2004), preprint).
Gordon D. Plotkin. The Origins of Structural Operational Semantics. J. Log. Algebr. Program. 60-61:3-15, 2004. (preprint).
Dana S. Scott. Outline of a Mathematical Theory of Computation, Programming Research Group, Technical Monograph PRG–2, Oxford University, 1970.
Adriaan van Wijngaarden et al. Revised Report on the Algorithmic Language ALGOL 68. IFIP. 1968. ([2]^{[permanent dead link]})
Matthew Hennessy. Semantics of Programming Languages. Wiley, 1990. available online.

외부 링크

Wikimedia Commons 운영 의미론 관련 매체

[1] McCarthy, John. "Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I". Archived from the original on 2013-10-04. Retrieved 2006-10-13.

[felleisen-hieb-92-2] Felleisen, M.; Hieb, R. (1992). "The Revised Report on the Syntactic Theories of Sequential Control and State". Theoretical Computer Science. 103 (2): 235–271. doi:10.1016/0304-3975(92)90014-7.

[3] Plotkin, Gordon (1975). "Call-by-name, call-by-value and the λ-calculus" (PDF). Theoretical Computer Science. 1 (2): 125–159. doi:10.1016/0304-3975(75)90017-1. Retrieved July 22, 2021.

[4] Felleisen, Matthias (1987). The calculi of Lambda-v-CS conversion: a syntactic theory of control and state in imperative higher-order programming languages (PDF) (PhD). Indiana University. Retrieved July 22, 2021.

[5] Felleisen, Matthias; Friedman, Daniel P. (1987). "A Reduction Semantics for Imperative Higher-Order Languages". Proceedings of the Parallel Architectures and Languages Europe. International Conference on Parallel Architectures and Languages Europe. Vol. 1. Springer-Verlag. pp. 206–223. doi:10.1007/3-540-17945-3_12.

[6] Abadi, M.; Cardelli, L. (8 September 2012). A Theory of Objects. ISBN 9781441985989.

[7] Felleisen, Matthias; Findler, Robert Bruce; Flatt, Matthew (2009). Semantics Engineering with PLT Redex. The MIT Press. ISBN 978-0-262-06275-6.

[8] 일리노이 대학교 CS422

[leroy-coinductivebigstep-9] 자비에 르로이."유도적인 큰 단계 운영 의미론"

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

Search

운용 의미론

네임스페이스

더

목차

역사