본문 바로가기
HOME> 논문 > 논문 검색상세

논문 상세정보

Information and computation v.261 pt.2, 2018년, pp.401 - 431  

Game semantics for dependent types

Vákár, Matthijs (Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, Oxford OX1 3QD, UK ) ; Jagadeesan, Radha (School of CTI, DePaul University, 243 S. Wabash Avenue, Chicago, IL 60604-2287, USA ) ; Abramsky, Samson (Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, Oxford OX1 3QD, UK ) ;
  • 초록  

    Abstract We present a model of dependent type theory ( DTT ) with Π-, 1-, Σ- and intensional Id -types, which is based on a slight variation of the (call-by-name) category of AJM-games and history-free winning well-bracketed strategies. The model satisfies Streicher's criteria of intensionality and refutes function extensionality. The principle of uniqueness of identity proofs is satisfied. We show it contains a submodel as a full subcategory which gives a faithful interpretation of DTT with Π-, 1-, Σ- and intensional Id -types and, additionally, finite inductive type families. This smaller model is fully (and faithfully) complete with respect to the syntax at the type hierarchy built without Id -types, as well as at the more general class of types where we allow for one strictly positive occurrence of an Id -type. Definability for the full type hierarchy with Id -types remains to be investigated.


  • 주제어

    Game semantics .   Dependent type theory .   Intensionality.  

 활용도 분석

  • 상세보기

    amChart 영역
  • 원문보기

    amChart 영역

원문보기

무료다운로드
  • 원문이 없습니다.
유료다운로드

유료 다운로드의 경우 해당 사이트의 정책에 따라 신규 회원가입, 로그인, 유료 구매 등이 필요할 수 있습니다. 해당 사이트에서 발생하는 귀하의 모든 정보활동은 NDSL의 서비스 정책과 무관합니다.

원문복사신청을 하시면, 일부 해외 인쇄학술지의 경우 외국학술지지원센터(FRIC)에서
무료 원문복사 서비스를 제공합니다.

NDSL에서는 해당 원문을 복사서비스하고 있습니다. 위의 원문복사신청 또는 장바구니 담기를 통하여 원문복사서비스 이용이 가능합니다.

이 논문과 함께 출판된 논문 + 더보기