{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T13:36:00Z","timestamp":1760708160738,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540230243"},{"type":"electronic","value":"9783540301240"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30124-0_20","type":"book-chapter","created":{"date-parts":[[2010,3,2]],"date-time":"2010-03-02T12:27:59Z","timestamp":1267532879000},"page":"235-249","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["A Dependent Type Theory with Names and Binding"],"prefix":"10.1007","author":[{"given":"Ulrich","family":"Sch\u00f6pp","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ian","family":"Stark","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2004,9,9]]},"reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/b11832","volume-title":"Foundations of Software Science and Computational Structures","author":"L. Cardelli","year":"2003","unstructured":"Cardelli, L., Gardner, P., Ghelli, G.: Manipulating trees with hidden labels. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol.\u00a02620, Springer, Heidelberg (2003)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_8","volume-title":"Typed Lambda Calculi and Applications","author":"L. Cardelli","year":"2001","unstructured":"Cardelli, L., Gordon, A.: Logical properties of name restriction. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol.\u00a02044, Springer, Heidelberg (2001)"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014049","volume-title":"Typed Lambda Calculi and Applications","author":"J. Despeyroux","year":"1995","unstructured":"Despeyroux, J., Felty, A., Hirschowitz, A.: Higher-order abstract syntax in Coq. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol.\u00a0902. Springer, Heidelberg (1995)"},{"key":"20_CR4","unstructured":"Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: Proceedings of LICS 1999 (1999)"},{"key":"20_CR5","unstructured":"Fiore, M., Turi, D.: Semantics of name and value passing. In: Proceedings of LICS 2001 (2001)"},{"key":"20_CR6","unstructured":"Gabbay, M.: FM-HOL, a higher-order theory of names. In: Workshop on Thirty Five years of Automath (2002)"},{"key":"20_CR7","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s001650200016","volume":"13","author":"M.J. Gabbay","year":"2002","unstructured":"Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing\u00a013, 341\u2013363 (2002)","journal-title":"Formal Aspects of Computing"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022273","volume-title":"Computer Science Logic","author":"M. Hofmann","year":"1995","unstructured":"Hofmann, M.: On the interpretation of type theory in locally cartesian closed categories. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol.\u00a0933, Springer, Heidelberg (1995)"},{"key":"20_CR9","unstructured":"Hofmann, M.: Semantical analysis of higher-order abstract syntax. In: Proceedings of LICS 1999 (1999)"},{"issue":"1\u20133","key":"20_CR10","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/S0168-0072(00)00010-5","volume":"104","author":"M. Hofmann","year":"2000","unstructured":"Hofmann, M.: Safe recursion with higher types and BCK-algebra. Annals of Pure and Applied Logic\u00a0104(1\u20133), 113\u2013166 (2000)","journal-title":"Annals of Pure and Applied Logic"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"963","DOI":"10.1007\/3-540-48224-5_78","volume-title":"Automata, Languages and Programming","author":"F. Honsell","year":"2001","unstructured":"Honsell, F., Miculan, M., Scagnetto, I.: An axiomatic approach to metareasoning on nominal algebras in HOAS. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, p. 963. Springer, Heidelberg (2001)"},{"key":"20_CR12","volume-title":"Categorical Logic and Type Theory","author":"B. Jacobs","year":"1999","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Elsevier Science, Amsterdam (1999)"},{"key":"20_CR13","volume-title":"Sketches of an Elephant: A Topos Theory Compendium","author":"P.T. Johnstone","year":"2002","unstructured":"Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium. Oxford University Press, Oxford (2002)"},{"key":"20_CR14","unstructured":"Lietz, P.: A fibrational theory of geometric morphisms. Master\u2019s thesis, TU Darmstadt (May 1998)"},{"key":"20_CR15","volume-title":"Sheaves in Geometry and Logic: A First Introduction to Topos Theory","author":"S. MacLane","year":"1992","unstructured":"MacLane, S., Moerdijk, I.: Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer, Heidelberg (1992)"},{"issue":"5","key":"20_CR16","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1023\/A:1025750816098","volume":"11","author":"M. Menni","year":"2003","unstructured":"Menni, M.: About N-quantifiers. Applied Categorical Structures\u00a011(5), 421\u2013445 (2003)","journal-title":"Applied Categorical Structures"},{"issue":"4","key":"20_CR17","doi-asserted-by":"publisher","first-page":"747","DOI":"10.1017\/S0956796802004495","volume":"13","author":"P. O\u2019Hearn","year":"2003","unstructured":"O\u2019Hearn, P.: On bunched typing. Journal of Functional Programming\u00a013(4), 747\u2013796 (2003)","journal-title":"Journal of Functional Programming"},{"key":"20_CR18","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"A.M. Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation\u00a0186, 165\u2013193 (2003)","journal-title":"Information and Computation"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722010_15","volume-title":"Mathematics of Program Construction","author":"A.M. Pitts","year":"2000","unstructured":"Pitts, A.M., Gabbay, M.J.: A metalanguage for programming with bound names modulo renaming. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol.\u00a01837, Springer, Heidelberg (2000)"},{"key":"20_CR20","volume-title":"The Semantics and Proof Theory of the Logic of Bunched Implications","author":"D. Pym","year":"1999","unstructured":"Pym, D.: The Semantics and Proof Theory of the Logic of Bunched Implications. Kluwer Academic Publishers, Dordrecht (1999)"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Seely, R.A.G.: Locally cartesian closed categories and type theory. In: Math. Proc. Cambridge Philos. Soc., vol.\u00a095, pp. 33\u201348 (1984)","DOI":"10.1017\/S0305004100061284"},{"key":"20_CR22","volume-title":"Practical Foundations of Mathematics","author":"P. Taylor","year":"1999","unstructured":"Taylor, P.: Practical Foundations of Mathematics. Cambridge University Press, Cambridge (1999)"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45220-1_41","volume-title":"Computer Science Logic","author":"C. Urban","year":"2003","unstructured":"Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol.\u00a02803, Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30124-0_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,22]],"date-time":"2020-01-22T20:03:42Z","timestamp":1579723422000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30124-0_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540230243","9783540301240"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30124-0_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]},"assertion":[{"value":"9 September 2004","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}