{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:35:11Z","timestamp":1750307711046,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":49,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,1,20]],"date-time":"2009-01-20T00:00:00Z","timestamp":1232409600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2009,1,20]]},"DOI":"10.1145\/1481848.1481851","type":"proceedings-article","created":{"date-parts":[[2009,1,20]],"date-time":"2009-01-20T14:41:38Z","timestamp":1232462498000},"page":"3-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Positively dependent types"],"prefix":"10.1145","author":[{"given":"Daniel R.","family":"Licata","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA, USA"}]},{"given":"Robert","family":"Harper","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA, USA"}]}],"member":"320","published-online":{"date-parts":[[2009,1,20]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289451"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/14.4.447"},{"key":"e_1_3_2_1_5_1","volume-title":"Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science","author":"Bertot Yves","year":"2004","unstructured":"Yves Bertot and Pierre Cast\u00e9ran . Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science . Springer , 2004 . Yves Bertot and Pierre Cast\u00e9ran. Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, 2004."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086397"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086375"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065022"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1762174.1762221"},{"key":"e_1_3_2_1_12_1","volume-title":"Implementing Mathematics with the NuPRL Proof Development System","author":"Constable Robert L.","year":"1986","unstructured":"Robert L. Constable , Stuart F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , Douglas J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , James T. Sasaki , and Scott F. Smith . Implementing Mathematics with the NuPRL Proof Development System . Prentice Hall , 1986 . Robert L. Constable, Stuart F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, Douglas J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, James T. Sasaki, and Scott F. Smith. Implementing Mathematics with the NuPRL Proof Development System. Prentice Hall, 1986."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317906"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964025"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/3-540-45504-3_7","volume-title":"Proof Theory in Computer Science","author":"Dybjer Peter","year":"2001","unstructured":"Peter Dybjer and Anton Setzer . Indexed induction-recursion . In Proof Theory in Computer Science , pages 93 -- 113 . Springer , 2001 . Peter Dybjer and Anton Setzer. Indexed induction-recursion. In Proof Theory in Computer Science, pages 93--113. Springer, 2001."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111059"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1244381.1244400"},{"key":"e_1_3_2_1_19_1","volume-title":"On the unity of logic. Annals of pure and applied logic, 59(3):201--217","author":"Girard Jean-Yves","year":"1993","unstructured":"Jean-Yves Girard . On the unity of logic. Annals of pure and applied logic, 59(3):201--217 , 1993 . Jean-Yves Girard. On the unity of logic. Annals of pure and applied logic, 59(3):201--217, 1993."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950100336X"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96744"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199475"},{"key":"e_1_3_2_1_24_1","volume-title":"Universit\u00e9 Aix-Marseille II","author":"Laurent Olivier","year":"2002","unstructured":"Olivier Laurent . Etude de la polarisation en logique. Th\u00e8se de doctorat , Universit\u00e9 Aix-Marseille II , March 2002 . Olivier Laurent. Etude de la polarisation en logique. Th\u00e8se de doctorat, Universit\u00e9 Aix-Marseille II, March 2002."},{"key":"e_1_3_2_1_25_1","unstructured":"Paul B. Levy. Call-by-push-value. PhD thesis Queen Mary University of London 2001.  Paul B. Levy. Call-by-push-value. PhD thesis Queen Mary University of London 2001."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Chuck\n      Liang\n     and \n      Dale\n      Miller\n    .\n  Focusing and polarization in intuitionistic logic\n  . In J. Duparc and T. A. Henzinger editors CSL \n  2007\n  : Computer Science Logic volume \n  4646\n   of \n  LNCS pages \n  451\n  --\n  465\n  . \n  Springer-Verlag 2007.   Chuck Liang and Dale Miller. Focusing and polarization in intuitionistic logic. In J. Duparc and T. A. Henzinger editors CSL 2007: Computer Science Logic volume 4646 of LNCS pages 451--465. Springer-Verlag 2007.","DOI":"10.1007\/978-3-540-74915-8_34"},{"key":"e_1_3_2_1_27_1","volume-title":"Dependently typed programming with domain-specific logics (thesis proposal). Available from http:\/\/www.cs.cmu.edu\/~drl","author":"Licata Daniel R.","year":"2008","unstructured":"Daniel R. Licata . Dependently typed programming with domain-specific logics (thesis proposal). Available from http:\/\/www.cs.cmu.edu\/~drl , 2008 . Daniel R. Licata. Dependently typed programming with domain-specific logics (thesis proposal). Available from http:\/\/www.cs.cmu.edu\/~drl, 2008."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.48"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.09.021"},{"key":"e_1_3_2_1_31_1","unstructured":"Keywords: LF refinement types subtyping dependent types intersection types  Keywords: LF refinement types subtyping dependent types intersection types"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70847-4"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/1754621.1754650"},{"key":"e_1_3_2_1_35_1","volume-title":"Intuitionistic Modal Logic and Applications","author":"Nanevski Aleksandar","year":"2005","unstructured":"Aleksandar Nanevski . A modal calculus for exception handling . In Intuitionistic Modal Logic and Applications , 2005 . Aleksandar Nanevski. A modal calculus for exception handling. In Intuitionistic Modal Logic and Applications, 2005."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159812"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159811"},{"key":"e_1_3_2_1_39_1","volume-title":"IEEE Symposium on Logic in Computer Science","author":"Pfenning Frank","year":"2001","unstructured":"Frank Pfenning . Intensionality, extensionality , and proof irrelevance in modal type theory . In IEEE Symposium on Logic in Computer Science , 2001 . Frank Pfenning. Intensionality, extensionality, and proof irrelevance in modal type theory. In IEEE Symposium on Logic in Computer Science, 2001."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328483"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/646794.704856"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792878.1792887"},{"key":"e_1_3_2_1_43_1","volume-title":"A cost-effective foundational certified code system. Thesis Proposal","author":"Sarkar Susmit","year":"2005","unstructured":"Susmit Sarkar . A cost-effective foundational certified code system. Thesis Proposal , Carenegie Mellon University , 2005 . Susmit Sarkar. A cost-effective foundational certified code system. Thesis Proposal, Carenegie Mellon University, 2005."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1053468.1053469"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1028664.1028711"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291156"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291201.1291206"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086400"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604150"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277732"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328482"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2008.01.001"},{"key":"e_1_3_2_1_54_1","unstructured":"Christoph Zenger. Indizierte Typen. PhD thesis Universitat Karlsruhe 1998.  Christoph Zenger. Indizierte Typen. PhD thesis Universitat Karlsruhe 1998."}],"event":{"name":"POPL09: The 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"],"location":"Savannah GA USA","acronym":"POPL09"},"container-title":["Proceedings of the 3rd workshop on Programming languages meets program verification"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1481848.1481851","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1481848.1481851","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:10Z","timestamp":1750253410000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1481848.1481851"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1,20]]},"references-count":49,"alternative-id":["10.1145\/1481848.1481851","10.1145\/1481848"],"URL":"https:\/\/doi.org\/10.1145\/1481848.1481851","relation":{},"subject":[],"published":{"date-parts":[[2009,1,20]]},"assertion":[{"value":"2009-01-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}