# Dependent type > 컴퓨터과학 또는 논리학에서 의존형이란 타입 정의가 값에 의존하는 타입을 말한다. 프로그래밍 언어 중 Lean, Idris, Coq 등이 의존형 시스템을 채택하고 있다. [컴퓨터과학](https://wiki.g15e.com/pages/Computer%20science.txt) 또는 <논리학>에서 의존형이란 타입 정의가 값에 의존하는 타입을 말한다. 프로그래밍 언어 중 [Lean](https://wiki.g15e.com/pages/Lean%20(programming%20language.txt)), , 등이 의존형 시스템을 채택하고 있다.