우리는 대수적 효과(algebraic effects)와 리전 기반 메모리 관리(region-based memory management)를 갖춘 새로운 ML 스타일의 프로그래밍 언어인 Yarrow를 선보입니다. 이러한 프로그래밍 언어 기능들을 하나의 언어로 조화시키는 것은 매우 도전적인 과제입니다. 대수적 효과의 비지역적 제어 흐름(non-local control flow)은 리전 기반 메모리 관리가 의존하는 함수 호출 및 반환의 스택 규율(stack discipline)을 깨뜨리며, 멀티샷 효과 핸들러(multi-shot effect handlers)는 리전이 최대 한 번만 종료될 수 있다는 불변성(invariant)을 깨뜨리기 때문입니다. 우리는 원샷(one-shot) 및 멀티샷 효과 핸들러가 존재하는 상황에서도 리전에 대한 안전하고 모듈식인 추론을 지원하는 Yarrow 로직(Yarrow Logic, YL)이라는 프로그램 로직을 제시합니다. 우리는 OCaml의 런타임에서 영감을 얻었으나 리전을 위해 정교화된 Yarrow의 운영 의미론(operational semantics)에 대해 이 로직이 건전함(sound)을 증명합니다. 우리는 YL을 사용하여 체크포인팅(checkpointing), 비동기 계산(asynchronous computation), 그리고 LIFO 데이터 구조 구현을 포함하여 대수적 효과를 사용하는 여러 사례 연구의 정확성을 증명합니다. 이러한 사례 연구에서 사용되는 모든 메모리 위치는 리전에 할당되므로, 이 사례 연구들은 효율성이 낮은 가비지 컬렉션(garbage collected) 힙 메모리 사용을 피할 수 있습니다. 우리는 Rocq Prover 상의 Iris 분리 로직(separation logic) 프레임워크를 사용하여 Yarrow의 운영 의미론, Yarrow 프로그램 로직, 그리고 모든 사례 연구를 정형화하였습니다.