Game semantics and uniqueness of type inhabitance in the simply-typed λ-calculus
作者： Pierre Bourreau , Sylvain Salvati
DOI: 10.1007/978-3-642-21691-6_8
关键词: Computer science 、 Intuitionistic logic 、 Calculus (medicine) 、 Uniqueness 、 Type (model theory) 、 Calculus 、 Coherence theorem 、 Game semantics 、 Principal (computer security) 、 Characterization (mathematics)
摘要: The problem of characterizing sequents for which there is a unique proof in intuitionistic logic was first raised by Mints [Min77], initially studied [BS82] and later [Aot99]. We address this through game semantics give new concise also fully characterize family λ-terms Aoto's theorem. use games leads to characterization principal typings simply-typed λ-terms. These results show that models can help proving strong structural properties the λ-calculus.
springer.com
archives-ouvertes.fr
core.ac.uk 
sci-hub.st 参考文章(23)
Pietro Di Gianantonio, Furio Honsell, Gianluca Franco, Game Semantics for Untyped lambda beta eta-Calculus international conference on typed lambda calculi and applications. pp. 114- 128 ,(1999)
Logical Foundations of Computer Science Lecture Notes in Computer Science. ,vol. 5407, ,(1994) , 10.1007/978-3-540-92687-0
J. Roger Hindley, Basic Simple Type Theory ,(1997)
Pietro Di Gianantonio, Gianluca Franco, Furio Honsell, Game Semantics for Untyped λβη-Calculus international conference on typed lambda calculi and applications. pp. 114- 128 ,(1999) , 10.1007/3-540-48959-2_10
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
Reinhard Muskens, Lambda grammars and the syntax-semantics interface Universiteit van Amsterdam. pp. 150- 155 ,(2001)
Sam Lindley, Extensional Rewriting with Sums Lecture Notes in Computer Science. pp. 255- 271 ,(2007) , 10.1007/978-3-540-73228-0_19
Hanno Nickau, Hereditarily sequential functionals Logical Foundations of Computer Science. pp. 253- 264 ,(1994) , 10.1007/3-540-58140-5_25
C. Barry Jay, Neil Ghani, The virtues of eta-expansion Journal of Functional Programming. ,vol. 5, pp. 135- 154 ,(1995) , 10.1017/S0956796800001301
G. E. Mints, Closed categories and the theory of proofs Journal of Soviet Mathematics. ,vol. 15, pp. 45- 62 ,(1981) , 10.1007/BF01404107