Type-Inhabitation: Formula-Trees vs. Game Semantics 1

作者： Sabine Broda , Sandra Alves

DOI:

关键词:

摘要:

暂无可下载资源，当前可以选择系统获取到有开放资源时通知我或者直接发起求助文献求助

参考文章(22)

Pierre Bourreau, Sylvain Salvati, A Datalog Recognizer for Almost Affine λ-CFGs Lecture Notes in Computer Science. pp. 21- 38 ,(2011) , 10.1007/978-3-642-23211-4_2

Pierre Bourreau, Sylvain Salvati, Game semantics and uniqueness of type inhabitance in the simply-typed λ-calculus international conference on typed lambda calculi and applications. ,vol. 6878, pp. 61- 75 ,(2011) , 10.1007/978-3-642-21691-6_8

Dag Prawitz, Natural Deduction: A Proof-Theoretical Study ,(1965)

Pawel Urzyczyn, Inhabitation in Typed Lambda-Calculi (A Syntactic Approach) international conference on typed lambda calculi and applications. pp. 373- 389 ,(1997) , 10.1007/3-540-62688-3_47

Sabine Broda, Luís Damas, Studying provability in implicational intuitionistic logic Electronic Notes in Theoretical Computer Science. ,vol. 67, pp. 131- 147 ,(2002) , 10.1016/S1571-0661(04)80545-0

Takahito Aoto, Uniqueness of Normal Proofs in Implicational Intuitionistic Logic Journal of Logic, Language and Information. ,vol. 8, pp. 217- 242 ,(1999) , 10.1023/A:1008254111992

Sabine Broda, Luís Damas, A Context-Free Grammar Representation for Normal Inhabitants of Types in TAlambda portuguese conference on artificial intelligence. pp. 321- 334 ,(2001) , 10.1007/3-540-45329-6_32

Paweł Urzyczyn, Inhabitation of Low-Rank Intersection Types international conference on typed lambda calculi and applications. pp. 356- 370 ,(2009) , 10.1007/978-3-642-02273-9_26

Sachio Hirokawa, Infiniteness of proof (a) is polynomial-space complete Theoretical Computer Science. ,vol. 206, pp. 331- 339 ,(1998) , 10.1016/S0304-3975(97)00168-0

Richard Statman, Intuitionistic propositional logic is polynomial-space complete Theoretical Computer Science. ,vol. 9, pp. 67- 72 ,(1979) , 10.1016/0304-3975(79)90006-9