%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % {LICS} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @InProceedings{aba03:lics, author = "M. Abadi", title = "Logic in Access Control", booktitle = "Proceedings of {LICS}'03", publisher = "IEEE Computer Society Press", year = "2003", pages = "228-233"} @InProceedings{peter91:lics, author = "P. Aczel", title = "Term Declaration Logic and Generalised Composita", booktitle = "Proceedings of {LICS}'91", publisher = "IEEE Computer Society Press", year = "1991", pages = "22--30"} @InProceedings{thorsten99:lics, author = "T. Altenkirch", title = "{Extensional Equality in Intensional Type Theory}", booktitle = "Proceedings of {LICS}'99", publisher = "IEEE Computer Society Press", year = "1999", pages={412--420} } @InProceedings{app01:lics, author = "A. W. Appel", title = "Foundational {Proof-Carrying} Code", pages = "247--258", booktitle = "Proceedings of {LICS}'01", publisher = "IEEE Computer Society", year = "2001", } @InProceedings{adriana96:lics, author={D. Aspinall and A. Compagnoni}, title={Subtyping Dependent Types}, booktitle = "Proceedings of {LICS}'96", publisher = "IEEE Computer Society Press", year={1996}, pages={86--97}} @InProceedings{aud91:lics, author={P. Audebaud}, title={{Partial Objects in the Calculus of Constructions}}, pages={86--95}, booktitle={Proceedings of {LICS}'91}, publisher = "IEEE Computer Society Press", year={1991}} @inproceedings{BFG94:lics, author={F. Barbanera and M. Fern{\'a}ndez and H. Geuvers}, title={Modularity of strong normalisation and confluence in the algebraic $\lambda$-cube}, booktitle={Proceedings of {LICS}'94}, pages={406-415}, publisher={IEEE Computer Society Press}, year={1994}} @inproceedings{BT88:lics, author={V. Breazu-Tannen}, title={Combining algebra and higher-order types}, booktitle={Proceedings of {LICS}'88}, year={1988}, publisher = "IEEE Computer Society Press", pages={82--90}} @InProceedings{BTKP93:lics, author = "V. Breazu-Tannen and D. Kesner and L. Puel", title = "A Typed Pattern Calculus", booktitle = "Proceedings of {LICS}'93", publisher = "IEEE Computer Society Press", year = 1993, } @Inproceedings{CKRT03:lics, author={Y. Chevalier and R. K{\"u}sters and M. Rusinowitch and M. Turuani}, title={{An NP Decision Procedure for Protocol Insecurity with XOR}}, booktitle={Proceedings of {LICS}'03}, pages={261-270}, year={2003}, publisher="IEEE Computer Society Press"} @Inproceedings{CS03:lics, author={H. Comon-Lundh and V. Shmatikov}, title="{Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or}", booktitle={Proceedings of {LICS}'03}, pages={271-280}, year={2003}, publisher="IEEE Computer Society Press"} @InProceedings{CS87:lics, author={R.L. Constable and S.F. Smith}, title={Partial Objects In Constructive Type Theory}, pages={183--193}, booktitle={Proceedings of {LICS}'87}, publisher={IEEE Computer Society Press}, year={1987} } @InProceedings{CS88:lics, author={R.L. Constable and S.F. Smith}, title={Computational Foundations of Basic Recursive Function Theory}, pages={360--371}, booktitle={Proceedings of {LICS}'88}, publisher={IEEE Computer Society Press}, year={1987} } @InProceedings{coq86:lics, author={T. Coquand}, title={An Analysis of {Girard's} Paradox}, pages={227--236}, booktitle={Proceedings of {LICS}'86}, year=1986, publisher={IEEE Computer Society Press}} @InProceedings{daw96:lics, title={A Temporal-Logic Approach to Binding-Time Analysis}, author={R. Davies}, pages={184--195}, booktitle={Proceedings of {LICS}'96}, publisher={IEEE Computer Society Press}, year={1996} } @inproceedings{herman92:lics, title={The {Church-Rosser} Property for $\beta\eta$-reduction in Typed $\lambda$-Calculi}, author={H. Geuvers}, pages={453--460}, booktitle={Proceedings of {LICS}'92}, publisher={IEEE Computer Society Press}, year={1992} } @inproceedings{GW94:lics, author={H. Geuvers and B. Werner}, title={On the {Church-Rosser} property for expressive type systems and its consequence for their metatheoretic study}, booktitle={Proceedings of {LICS}'94}, pages={320-329}, publisher={IEEE Computer Society Press}, year={1994}} @InProceedings{GM87:lics, author = "J. Goguen and J. Meseguer", title = "Order-Sorted Algebra solves the Constructor-Selector, Multiple", pages = "18--29", booktitle = "Proceedings of {LICS}'86", year = "1986", publisher = "IEEE Computer Society"} @InProceedings{shao+02:lics, author = "N.A. Hamid and Z. Shao and V. Trifonov and S. Monnier and Z. Ni", title = "A Syntactic Approach to Foundational Proof-Carrying Code", pages = "89--100", booktitle = "Proceedings of {LICS}'02", publisher = "IEEE Computer Society", year = "2002"} @inproceedings{HHP87:lics, author="R. Harper and F. Honsell and G. Plotkin", title="A Framework for Defining Logics", booktitle="Proceedings of {LICS}'87", year=1987, pages="194--204", publisher = "IEEE Computer Society Press"} @InProceedings{HJ92:lics, title = "An {E}ngine for {L}ogic {P}rogram {A}nalysis", author = "N. Heintze and J. Jaffar", pages = "318--328", booktitle = "Proceedings of {LICS}'92", year = "1992", publisher={IEEE Computer Society Press} } @InProceedings{HS94:lics, title={The Groupoid Model Refutes Uniqueness of Identity Proofs}, author={M. Hofmann and T. Streicher}, pages={208--212}, booktitle={Proceedings of {LICS}'94}, year=1994, publisher={IEEE Computer Society Press} } @inproceedings{HS97:lics, title={Continuation Models are Universal for $\lambda\mu$-calculus}, author={M. Hofmann and T. Streicher}, booktitle={Proceedings of {LICS}'97}, publisher={IEEE Computer Society Press}, year={1997}} @InProceedings{how87:lics, author = "D. Howe", title = "The Computational Behaviour of {Girard's} Paradox", pages = "205--214", booktitle = "Proceedings of {LICS}'87", year = "1987", publisher = "IEEE Computer Society Press", } @inproceedings{JO91:lics, author={J.-P. Jouannaud and M. Okada}, title={Executable higher-order algebraic specification languages}, booktitle={Proceedings of {LICS}'91}, pages={350-361}, publisher = "IEEE Computer Society Press", year={1991}} @InProceedings{KW95:lics, title={New Notions of Reduction and Non-Semantic Proofs of {$\beta$}-Strong Normalization in Typed {$\lambda$}-Calculi}, author={A.J. Kfoury and J.B. Wells}, pages={311--321}, booktitle={Proceedings of {LICS}'95}, publisher={IEEE Computer Society Press}, year={1995} } @InProceedings{men87:lics, author = "N. P. Mendler", title = "Inductive Types and Type Constraints in Second-order Lambda Calculus", year = "1987", booktitle = "Proceedings of {LICS}'87", pages={30-36}, publisher="IEEE Computer Society Press"} @inproceedings{mid89:lics, author={A. Middeldorp}, title={A sufficient condition for the termination of the direct sum of term-rewriting systems}, booktitle={Proceedings of {LICS}'89}, pages={396-401}, year={1989}, publisher="IEEE Computer Society Press"} @InProceedings{chet91:lics, author={C. Murthy}, title={An Evaluation Semantics for Classical Proofs}, pages={96--107}, booktitle={Proceedings of {LICS}'91}, publisher = "IEEE Computer Society Press", year={1991}} @InProceedings{NL98:lics, author = "G.C. Necula and P. Lee", title = "Efficient Representation and Validation of Logical Proofs", booktitle = "Proceedings of LICS'98", pages = "93--104", year = "1998"} @InProceedings{ong96:lics, author = {Ong, C.-H. L.}, title = {A Semantic View of Classical Proofs: Type-theoretic, Categorical, and Denotational Characterizations}, booktitle ={Proceedings of {LICS}'96}, publisher = "IEEE Computer Society Press", year={1996}, pages={230--241}} @InProceedings{pal94:lics, title={Efficient Inference of Object Types}, author={J. Palsberg}, pages={186--195}, booktitle={Proceedings of {LICS}'94}, publisher = "IEEE Computer Society Press", year={1994}} @InProceedings{PZ00:lics, author = "J. Palsberg and T. Zhao", title = "Efficient and Flexible Matching of Recursive Types", pages = "388--400", booktitle = "Proceedings of {LICS}'00", publisher = "IEEE Computer Society Press", year = "2000", } @InProceedings{par93:lics, title={Strong Normalization for Second Order Classical Natural Deduction}, author={M. Parigot}, pages={39--46}, booktitle={Proceedings of {LICS}'93}, publisher = "IEEE Computer Society Press", year={1993}} @InProceedings{pip95:lics, title={Normalization and Extensionality (Extended Abstract)}, author={A. Piperno}, pages={300--310}, year={1995}, booktitle={Proceedings of {LICS}'95}, publisher={IEEE Computer Society Press}} @INPROCEEDINGS{pit89:lics, AUTHOR={A.~M.~Pitts}, TITLE={Non-trivial Power Types Can't Be Subtypes of Polymorphic Types}, BOOKTITLE={Proceedings of {LICS}'89}, PUBLISHER={IEEE Computer Society Press}, YEAR=1989, PAGES={6--13}} @inproceedings{pfe89:lics, author = "F. Pfenning", title="Elf: A Language for Logic Definition and Verified Metaprogramming", booktitle="Proceedings of {LICS}'89", publisher = "IEEE Computer Society Press", year=1989 } @InProceedings{SS88:lics, author={A. Salvesen and J. Smith}, title={{The Strength of the Subset Type in {Martin-L{\"o}f's} Type Theory}}, pages={384--391}, booktitle={Proceedings of {LICS}'88}, publisher={IEEE Computer Society Press}, year=1988} @InProceedings{see87:lics, author={R. Seely}, title={Modelling Computations: A 2-Categorical Framework}, pages={65--71}, booktitle={Proceedings of {LICS}'87}, publisher={IEEE Computer Society Press}, year={1987} } @InProceedings{vis98:lics, title={Full Abstraction for First-Order Objects with Recursive Types and Subtyping}, author={R. Viswanathan}, pages={xxx--xxx}, booktitle={Proceedings of {LICS}'98}, publisher={IEEE Computer Society Press}, year={1998} } @inproceedings{wel94:lics, title={Typability and Type-Checking in the Second-Order $\lambda$-Calculus are Equivalent and Undecidable}, author={J.B. Wells}, pages={176--185}, booktitle={Proceedings of {LICS}'94}, publisher={IEEE Computer Society Press}, year={1994}} @inproceedings{xi01:lics, author = "H. Xi", title = {{Dependent Types for Program Termination Verification}}, booktitle = "Proceedings of {LICS}'01", year = 2001, publisher={IEEE Computer Society Press}, pages = "231--242" } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % POPL % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @InProceedings{ABHR99:popl, title={A core calculus of dependency}, booktitle={Proceedings of {POPL}'99}, year={1999}, author={M. Abadi and A. Banerjee and N. Heintze and J. Riecke}, publisher = "ACM Press", pages={147--160}} @InProceedings{aga00:popl, author = "J. Agat", title = "Transforming Out Timing Leaks.", pages = "40--53", booktitle = "Proceedings of POPL'00", publisher = "ACM Press", year = "2000", } @inproceedings{AC91:popl, author={R. Amadio and L. Cardelli}, title={Subtyping recursive types}, booktitle={Proceedings of {POPL}'91}, year={1991}, publisher={ACM Press}, pages={104--118}} @InProceedings{ABB06:popl, title = "A logic for information flow in object-oriented programs", author = "T. Amtoft and S. Bandhakavi and A. Banerjee", booktitle = "Proceedings of {POPL}'06", publisher = "ACM Press", year = "2006", pages = "91--102" } @InProceedings{AF00:popl, author = "A.W. Appel and A.P. Felty", title = "A Semantic Model of Types and Machine Instuctions for Proof-Carrying Code", pages = "243--253", booktitle = "Proceedings POPL'00", publisher = "ACM Press", year = "2000"} @inproceedings{ben04:popl, author = "N. Benton", title = "Simple relational correctness proofs for static analyses and program transformations", booktitle="Proceedings of POPL'04", pages = "14--25", publisher = "ACM Press", year = "2004" } @inproceedings{BM92:popl, author={K. Bruce and J. Mitchell}, title={{PER} models of subtyping, recursive types and higher-order polymorphism}, booktitle={Proceedings of {POPL}'92}, year={1992}, publisher={ACM Press}, pages={316-327}} @InProceedings{BM97:popl, title={Type-Checking Higher-Order Polymorphic Multi-Methods}, author={F. Bourdoncle and S. Merz}, pages={302--315}, booktitle ={Proceedings of {POPL}'97}, publisher ={ACM Press}, year ="1997" } @inproceedings (car88:popl, author = "L. Cardelli", title = "Structural Subtyping and the Notion of Power Type", booktitle = "Proceedings of {POPL}'88", year = 1988, pages = "70-79", publisher={ACM Press}) @InProceedings{CGL92:popl, author = "E. M. Clarke and O. Grumberg and D. E. Long", title = "Model checking and abstraction", booktitle = "Proceedings of {POPL}'92", publisher = "ACM Press", year = "1992", pages = "343--354", year = "1992" } @InProceedings{CF00:popl, author = "T. Colcombet and P. Fradet", title = "Enforcing Trace Properties by Program Transformation", pages = "54--66", booktitle = "Proceedings of {POPL}'00", publisher = "ACM Press", year = "2000", } @inproceedings{cou97:popl, author = {Cousot, P{.}}, title = {Types as Abstract Interpretations, invited paper}, pages = {316--331}, booktitle = {Proceedings of {POPL}'97}, publisher = "ACM Press", year = 1997 } @InProceedings{CC77:popl, title={Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints}, author={P. Cousot and R. Cousot}, pages={238--252}, booktitle = "Proceedings of {POPL}'77", year = 1977, publisher = "ACM Press" } @InProceedings{CW00:popl, author = "K. Crary and S. Weirich", title = "Resource Bound Certification", pages = "184--198", booktitle = "Proceedings of {POPL}'00", publisher = "ACM Press", year = "2000", } @InProceedings{olivier96:popl, author = "O. Danvy", title = "Type-Directed Partial Evaluation", booktitle = "Proceedings of {POPL}'96", year = 1996, publisher = "ACM Press", pages = "242--257" } @InProceedings{dam06:popl, title = "Decidability and proof systems for language-based noninterference relations", author = "M. Dam", booktitle = "Proceedings of {POPL}'06", publisher = "ACM Press", year = "2006", pages = "67--78"} @inproceedings{DM82:popl, author = "L. Damas and R. Milner", title = "Principal type schemes for functional programs", booktitle="Proceedings of {POPL}'82", year = "1982", publisher = "ACM Press", pages = "207--212"} @InProceedings{DP96:popl, author = "R. Davies and F. Pfenning", title = "A Modal Analysis of Staged Computation", booktitle = "Proceedings of {POPL}'96", year = 1996, publisher = "ACM Press", pages = "258--270" } @InProceedings{DHM91:popl, title={Typing First-Class Continuations in {ML}}, author={B.F. Duba and R. Harper and D. MacQueen}, booktitle={Proceedings of {POPL}'91}, pages={163--173}, year={1991}, publisher={ACM Press} } @InProceedings{fel88:popl, title={The Theory and Practice of First-Class Prompts}, author={M. Felleisen}, booktitle={Proceedings of {POPL}'88}, pages={180--190}, year={1988}, publisher={ACM Press} } @inproceedings{FS01:popl, author = {C. Flanagan and J.B. Saxe}, title = {Avoiding exponential explosion: generating compact verification conditions}, booktitle = {Proceedings of POPL'01}, year = {2001}, pages = {193--205}, publisher = {ACM Press} } @InProceedings(futelal85:popl ,Author="K. Futatsugi and J. Goguen and J.-P. Jouannaud and J. Meseguer" ,Title="Principles of {OBJ}2." ,Booktitle="Proceedings of {POPL}'85" ,Pages="52--66" ,Year=1985 ,publisher={ACM Press}) @inproceedings{GM04:popl, author = {R. Giacobazzi and I. Mastroeni}, title = {Abstract Non-Interference: Parameterizing Non-Interference by Abstract Interpretation}, booktitle = {Proceedings of {POPL}'04}, pages = {186-197}, year={2004}, publisher={ACM Press} } @InProceedings{GR96:popl, title={Bisimilarity for a First-Order Calculus of Objects with Subtyping}, author={A.D. Gordon and G.D. Rees}, pages={386--395}, booktitle={Proceedings of {POPL}'96}, year={1996}, publisher={ACM Press} } @inproceedings{GS01:popl, author = "A.D. Gordon and D. Syme", title = "Typing a multi-language intermediate code", booktitle={Proceedings of {POPL}'01}, year = "2001", publisher={ACM Press}, pages = "248--260"} @InProceedings{gri90:popl, title={A Formulae-as-Types Notion of Control}, author={T. Griffin}, year={1990}, pages={47--58}, booktitle={Proceedings of {POPL}'90}, publisher={ACM Press}} @InProceedings{HD94:popl, title={A Generic Account of Continuation-Passing Styles}, author={J. Hatcliff and O. Danvy}, pages={458--471}, year={1994}, booktitle={Proceedings of {POPL}'94}, publisher={ACM Press}} @InProceedings{HHM90:popl, author = "R. Harper and J. C. Mitchell and E. Moggi", title = "Higher-order modules and the phase distinction", booktitle = "Proceedings of {POPL}'90", year = "1990", pages = "341--354", publisher={ACM Press}} @InProceedings{HL93:popl, title={Explicit Polymorphism and {CPS} Conversion}, author={R. Harper and M. Lillibridge}, booktitle={Proceedings of {POPL}'93}, pages={206--219}, year={1993}, publisher={ACM Press}} @INPROCEEDINGS{HM95:popl, booktitle ={Proceedings of {POPL}'95}, AUTHOR = {R. Harper and G. Morrisett}, TITLE = {{Compiling Polymorphism Using Intensional Type Analysis}}, YEAR = 1995, PAGES = {130-141}, publisher = "ACM Press" } @InProceedings{HJ90:popl, title={A Finite Presentation Theorem for Approximating Logic Programs}, author={N. Heintze and J. Jaffar}, booktitle={Proceedings of {POPL}'90}, pages={197--209}, publisher ="ACM Press", year={1995} } @inproceedings{HR98:popl, author={N. Heintze and J. Riecke}, title={The {SLam} calculus: programming with secrecy and integrity}, booktitle={Proceedings of {POPL}'98}, year=1998, publisher={ACM Press}, pages={365--377}} @InProceedings{hin00:popl, author = "R. Hinze", title = "A New Approach to Generic Functional Programming.", pages = "119--132", booktitle = "Proceedings of {POPL}'00", publisher = "ACM Press", year = "2000", } @InProceedings{HJ03:popl, author = "M. Hofmann and S. Jost", title = "Static prediction of heap space usage for first-order functional programs", pages = "185--197", booktitle = "Proceedings of {POPL}'03", month = jan # " ~15--17", series = "ACM SIGPLAN Notices", volume = "38, 1", publisher = "ACM Press", year = "2003"} @InProceedings{HY02:popl, author = "K. Honda and N. Yoshida", title = "{A Uniform Type Structure for Secure Information Flow}", booktitle = "Proceedings of {POPL}'02", publisher="ACM Press", year = "2002", pages = "81--92", } @InProceedings{HPS96:popl, title = "Proving the Correctness of Reactive Systems Using Sized Types", author = "J. Hughes and L. Pareto and A. Sabry", pages = "410--423", booktitle = "Proceedings of {POPL}'96", year = "1996", publisher={ACM Press} } @InProceedings{JW95:popl, title={A Unified Treatment of Flow Analysis in Higher-Order Languages}, author={S. Jagannathan and S. Weeks}, pages={393--407}, booktitle={Proceedings of {POPL}'95}, year=1995, publisher={ACM Press} } @InProceedings{JTWW98:popl, title={Single and loving it: Must-alias analysis for higher-order languages}, author={S. Jagannathan and P. Thiemann and S. Weeks and A. Wright}, pages={329--341}, booktitle={Proceedings of {POPL}'98}, year=1998, publisher={ACM Press} } @InProceedings{JJ97:popl, title = "{PolyP}---a polytypic programming language extension", author = "P. Jansson and J. Jeuring", pages = "470--482", booktitle = "Proceedings of {{POPL}}'97", year = "1997", publisher = "ACM Press"} @InProceedings{jim96:popl, author = "T. Jim", title = "What are principal typings and what are they good for?", booktitle = "Proceedings of {POPL}'96", year = 1996, publisher = "ACM Press", pages = "42--53" } @InProceedings{JM82:popl, author = "N. D. Jones and S. S. Muchnick", title = "A Flexible Approach to Interprocedural Flow Analysis and Programs with Recursive Data Structures", booktitle = "Proceedings of {POPL}'82", publisher = "ACM Press", year = "1982" } @InProceedings{kil73:popl, author = "G. A. Kildall", title = "A Unified Approach to Global Program Optimization", booktitle = "Proceedings of {POPL}'73", year = "1973", publisher = "ACM Press", pages = "194--206" } @inproceedings{lei83:popl, AUTHOR = "Leivant, D.", BOOKTITLE ={Proceedings of {POPL}'83}, ORGANIZATION = "ACM", PAGES = "88--98", TITLE = "Polymorphic Type Inference", YEAR = "1983"} @inproceedings{mil+05:popl, title="Automated Soundness Proofs for Dataflow Analyses and Transformations via Local Rules", author="S. Lerner and T. Millstein and E. Rice and C. Chambers", booktitle="Proceedings of {POPL}'05", year={2005}, publisher = "ACM Press", pages="364-377"} @InProceedings{ler06:popl, author = {X. Leroy}, title = "Formal certification of a compiler back-end, or: programming a compiler with a proof assistant", booktitle = "Proceedings of {POPL}'06", year={2006}, pages="42-54", publisher = "ACM Press"} @InProceedings{ler93:popl, author = {X. Leroy}, title = "Polymorphism by Name for References and Continuations", booktitle = "Proceedings of {POPL}'93", pages = "220-231", year={1993}, publisher = "ACM Press"} @InProceedings{neil+01:popl, title={The Size-Change Principle for Program Termination}, author={C.-S. Lee and N. D. Jones and A. M. Ben-Amram}, booktitle = "Proceedings of {POPL}'01", year={2001}, pages={81--92}, publisher = "ACM Press"} @InProceedings{McQ86:popl, title={Using dependent types to express modular structure}, author={D. MacQueen}, pages={277-286}, booktitle ={Proceedings of {POPL}'86}, publisher ={ACM Press}, year ="1986"} @InProceedings{MR86:popl, title={{``Type''} Is Not A Type}, author={A.R. Meyer and M.B. Reinhold}, pages={287--295}, booktitle ={Proceedings of {POPL}'86}, publisher ={ACM Press}, year ="1986"} @InProceedings{MMH96:popl, author = "Y. Minamide and G. Morrisett and R. Harper", title = "Typed Closure Conversion", booktitle= "Preceedings of {POPL}'96", pages = "271-283", year={1996}, publisher = "ACM Press" } @inproceedings{mit90:popl, author={J. Mitchell}, title={Towards a typed foundation for method specialisation and inheritance}, booktitle={Proceedings of {POPL}'90}, year={1990}, publisher={ACM Press}, pages={109--124}} @InProceedings{mor+98:popl, author = "G. Morrisett and D. Walker and K. Crary and N. Glew", title = "From System~{F} to Typed Assembly Language", booktitle = "Proceedings of POPL'98", year = "1998", publisher = "ACM Press", pages = "85--97"} @InProceedings{mye99:popl, title={JFlow: Practical Mostly-Static Information Flow Control}, booktitle={Proceedings of {POPL}'99}, year={1999}, author={A.C. Myers}, publisher = "ACM Press", pages={228--241}} @InProceedings{nec97:popl, author = "G.C. Necula", title = "{Proof-Carrying Code}", booktitle = "{Proceedings of POPL'97}", year = "1997", pages = "106--119", publisher={ACM Press}} @InProceedings{NR01:popl, author = "G.C. Necula and S.P. Rahul", title = "Oracle-based checking of untrusted software", pages = "142--154", booktitle = "Proceedings of POPL'01", series = "ACM SIGPLAN Notices", volume = "36", issue=3, publisher = "ACM Press", year = "2001"} @inproceedings{thi+02:popl, author = "M. Neubauer and P. Thiemann and M. Gasbichler and M. Sperber", title = "Functional logic overloading", pages = "233--244", year={2002}, publisher={ACM Press}, booktitle = "Proceedings of POPL'02"} @InProceedings{NN97:popl, title={Infinitary Control Flow Analysis: a Collecting Semantics for Closure Analysis}, author={F. Nielson and H. R. Nielson}, pages={332--345}, booktitle={Proceedings of {POPL}'97}, year={1997}, publisher={ACM Press} } @InProceedings{NvO98:popl, title={{Java$_{\mathit{light}}$} is Type-Safe---Definitely}, author={T. Nipkow and D. von Oheimb}, pages={161--170}, booktitle={Proceedings of {POPL}'98}, year={1998}, publisher={ACM Press} } @InProceedings{OL96:popl, title={Putting Type Annotations to Work}, author={M. Odersky and K. L{\"a}ufer}, pages={54--67}, booktitle={Proceedings of {POPL}'96}, year={1996}, publisher={ACM Press}} @Inproceedings{OS97:popl, author = "C.-H.L. Ong and C.A. Stewart", title = "A {Curry-Howard Foundation} for functional computation with control", booktitle ={Proceedings of {POPL}'97}, publisher ={ACM Press}, pages={??--??}, year ="1997"} @InProceedings{PP98:popl, title={From Polyvariant Flow Information to Intersection and Union Types}, author={J. Palsberg and C. Pavlopoulou}, pages={197--208}, year={1998}, booktitle={Proceedings of {POPL}'98}, publisher = "ACM Press"} } @Inproceedings{PJetal98:popl, author = "S. {Peyton Jones} and J. Launchbury and M. Shields and A. Tolmach", title = "The Design of a Typed Intermediate Language", year={1998}, booktitle={Proceedings of {POPL}'98}, publisher = "ACM Press"} @INPROCEEDINGS{PJW93:popl, booktitle ="Proceedings of {POPL}'93", AUTHOR = {S.L. {Peyton Jones} and P.L. Wadler}, TITLE = {Imperative Functional Programming}, PAGES = {71-84}, YEAR = 1993, publisher = "ACM Press"} @InProceedings{PT98:popl, title={Local Type Inference}, author={B.C. Pierce and D.N. Turner}, pages={252--265}, YEAR = 1998, publisher = "ACM Press", booktitle ="Proceedings of {POPL}'98"} @InProceedings{PS02:popl, author = "F. Pottier and V. Simonet", title = "Information flow inference for {ML}", booktitle = "Proceedings of {POPL}'02", publisher="ACM Press", year = "2002", pages={319--330}} @InProceedings{RV97:popl, title={Objective {ML}: A simple object-oriented extension of~{ML}}, author={D. R{\'e}my and J. Vouillon}, pages={40--53}, booktitle ={Proceedings of {POPL}'97}, publisher ={ACM Press}, year ="1997" } @InProceedings{riv04:popl, author={X. Rival}, title={{Symbolic Transfer Functions-based Approaches to Certified Compilation}}, booktitle={Proceedings of {POPL}'04}, publisher ={ACM Press}, pages={1--13}, year ="2004"} @Inproceedings{amok97:popl, author = "A. Saibi", title = "{Typing Algorithm in Type Theory with Inheritance}", booktitle ={Proceedings of {POPL}'97}, publisher ={ACM Press}, pages={292--301}, year ="1997"} @Inproceedings{sch98:popl, author={A. Schubert}, title={Second-order unification and type inference for Church-style polymorphism}, year={1998}, booktitle={Proceedings of {POPL}'98}, publisher = "ACM Press", pages={279--288}} @InProceedings{shao+02:popl, author = "Z. Shao and B. Saha and V. Trifonov and N. Papaspyrou", title = "A Type System for Certified Binaries", pages = "217--232", booktitle = "Proceedings of POPL'02", year={2002}, publisher={ACM Press} } @InProceedings{SH97:popl, title = "Fast and Accurate Flow-Insensitive Points-To Analysis", author = "M. Shapiro and S. Horwitz", pages = "1--14", booktitle = "Proceedings of {POPL}'97", publisher = "ACM Press", year = "1997"} @InProceedings{SV98:popl, title={Secure Information Flow in a Multi-threaded Imperative Language}, author={G. Smith and D. Volpano}, pages={355--364}, year={1998}, booktitle={Proceedings of {POPL}'98}, publisher = "ACM Press"} @InProceedings{SA98:popl, title={A Type System for {Java} Bytecode Subroutines}, author={R. Stata and M. Abadi}, pages={149--160}, year={1998}, booktitle={Proceedings of {POPL}'98}, publisher = "ACM Press" } @Inproceedings{ste96:popl, author = "B. Steensgard", title = "Points-to analysis in almost linear time", booktitle ={Proceedings of {POPL}'96}, publisher ={ACM Press}, pages={32--41}, year ="1996"} @InProceedings{SH00:popl, author = "C. A. Stone and R. Harper", title = "{Deciding Type Equivalence with Singleton Kinds}", pages = "214--227", booktitle = "Proceedings of {POPL}'00", publisher = "ACM Press", year = "2000", } @InProceedings{VS00:popl, author = "D. M. Volpano and G. Smith", title = "Verifying Secrets and Relative Secrecy.", pages = "268--276", booktitle = "Proceedings of {POPL}'00", publisher = "ACM Press", year = "2000", } @InProceedings{wad87:popl, title={Views: A Way for Pattern Matching to Cohabit with Data Abstraction}, author={P. Wadler}, pages={307--313}, year={1987}, booktitle={Proceedings of {POPL}'87}, publisher={ACM Press}} @inproceedings{WB89:popl, author={P. Wadler and S. Blott}, title={How to make ad hoc polymorphism less ad hoc}, year={1989}, pages={60-76}, booktitle={Proceedings of {POPL}'89}, publisher={ACM Press}} @inproceedings{wad92:popl, author={P. Wadler}, title={The essence of functional programming}, year={1992}, pages={1--14}, booktitle={Proceedings of {POPL}'92}, publisher={ACM Press}} @InProceedings{wal00:popl, author = "D. Walker", title = "{A Type System for Expressive Security Policies}", pages = "254--267", booktitle = "Proceedings of {POPL}'00", publisher = "ACM Press", year = "2000", } @InProceedings{WS99:popl, author = {M. Wand and I. Siveroni}, title = {Constraint Systems for Useless Variable Elimination}, booktitle = {Proceedings of {POPL}'99}, year = 1999, pages = {291--302} } @InProceedings{XP99:popl, title={Dependent Types in Practical Programming}, booktitle={Proceedings of {POPL}'99}, year={1999}, author={H. Xi and F. Pfenning}, pages={214-227}, publisher ="ACM Press"} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % FPCA+ LFP % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @InProceedings{ber90:lfp, author = "A. Berlin", title = "Partial evaluation applied to numerical computation", booktitle = "Proceedings of LFP'90", publisher = "ACM Press", year = "1990", pages = "139--150"} @inproceedings (CCHMO89:fpca, author = "P. Canning and W. Cook and W. Hill and J. Mitchell and W. Olthoff", title = "F-Bounded Quantification for Object-Oriented Programming", booktitle = "Proceedings of FPCA'89", year = "1989", pages = "273--280") @InProceedings{CDDK86:lfp, author = "D. Clement and J. Despeyroux and T. Despeyroux and G. Kahn", title = "A simple applicative language: Mini-{ML}", booktitle = "Proceedings of LFP'86", publisher = "ACM Press", year = "1986", pages = "13--27"} @inproceedings{DL92:lfp, author={O. Danvy and J. Lawall}, title={Back to direct style {II}: First-class continuations}, booktitle={Proceedings of LFP'92}, year={1992}, pages={299-310}, publisher={ACM Press} } @inproceedings{OWW95:fpca, author = "M. Odersky and P. Wadler and M. Wehr", title = "A Second Look at Overloading", booktitle = "Proceedings of FPCA'95", pages = {135-146}, year = 1995, publisher={ACM Press}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % ICFP % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @InProceedings{aug98:icfp, author={L. Augustsson}, title={Cayenne: A language with dependent types}, year={1998}, booktitle={Proceedings of {ICFP}'98}, pages={239--250}, publisher = "ACM Press"} @InProceedings{DHT97:icfp, author = "D. Dussart and J. Hughes and P. Thiemann", title = "Type Specialisation for Imperative Languages", pages = "204-216", booktitle = " Proceedings of ICFP'97", year = 1997, publisher = "ACM Press" } @InProceedings{GL02:icfp, author = {B. Gr{\'e}goire and X. Leroy}, title = "A compiled implementation of strong reduction", booktitle = "Proceedings of {ICFP}'02", year={2002}, publisher = "ACM Press"} @InProceedings{gro01:icfp, author = "B. Grobauer", title = "Cost Recurrences for {DML} Programs", pages = "253--264", booktitle = "Proceedings of {ICFP}'01", publisher = "ACM Press", year = "2001", } @inproceedings{HO03:icfp, author = "T. Higuchi and A. Ohori", title = "A static type system for {JVM} access control", booktitle = "Proceedings of {ICFP}'03", pages = "227--237", year = "2003", publisher = "ACM Press", } @InProceedings{HMcA97:icfp, title = "On the Complexity of Set-Based Analysis", author = "N. Heintze and D. McAllester", pages = "150--163", booktitle = "Proceedings of ICFP'97", year = "1997", publisher = "ACM Press" } @InProceedings{MW97:icfp, title={A Practical Subtyping System for {Erlang}}, author={S. Marlow and P. Wadler}, pages={136--149}, booktitle = " Proceedings of ICFP'97", year = 1997, publisher = "ACM Press" } @InProceedings{nor98:icfp, title={Pragmatic Subtyping in Polymorphic Languages}, author={J. Nordlander}, booktitle = " Proceedings of ICFP'98", year = 1998, publisher = "ACM Press", pages={216-227}} @InProceedings{pot98:icfp, title={A Framework for Type Inference with Subtyping}, author={F. Pottier}, booktitle = " Proceedings of ICFP' 98", year = 1998, publisher = "ACM Press" } @InProceedings{SW96:icfp, author = "A. Sabry and P. Wadler", title = "A Reflection on Call-by-value", booktitle = "Proceedings of ICFP'96", pages = "13-24", year={1996}, publisher = "ACM Press"} @InProceedings{XH01:icfp, author = "H. Xi and R. Harper", title = "{A Dependently Typed Assembly Language}", pages = "169--180", booktitle = "Proceedings of {ICFP}'01", publisher = "ACM Press", year = "2001", } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % PLDI % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @INPROCEEDINGS{nec+00:pldi, author = "C. Colby and P. Lee and G.C. Necula and F. Blau and M. Plesko and K. Cline", title = "A certifying compiler for {J}ava", pages = "95--107", booktitle = "Proceedings of {PLDI}'00", OPTmonth = jun, OPTseries = "ACM Sigplan Notices", OPTvolume = "35", OPTissue=5, publisher = "ACM Press", year = "2000", } @InProceedings{CFS90:pldi, author = "R. Cytron and J. Ferrante and V. Sarkar", title = "Compact Representations for Control Dependence", booktitle = "Proceedings of {PLDI}'90", year = "1990", publisher = "ACM Press", pages = "337--351"} @INPROCEEDINGS{FSDF93:pldi, booktitle ="Proceedings of {PLDI}'93", AUTHOR = {C. Flanagan and A. Sabry and B.F. Duba and M. Felleisen}, TITLE = {The Essence of Compiling with Continuations}, YEAR = 1993, PAGES = {237-247} } @InProceedings{FF97:pldi, author = "C. Flanagan and M. Felleisen", title = "Componential Set-Based Analysis", pages = "235--248", booktitle = "Proceedings of {PLDI}'97", series = "ACM SIGPLAN Notices", volume = "32", issue=" 5", publisher = "ACM Press", year = "1997" } @InProceedings{FF00:pldi, author = "C. Flanagan and S.N. Freund", title = "Type-based race detection for Java", pages = "219--232", booktitle = "Proceedings of PLDI'00", series = "ACM Sigplan Notices", volume = "35", issue=2, publisher = "ACM Press", year = "2000"} @Inproceedings{FQ03:pldi, author = "C. Flanagan and S. Qadeer", title = "A type and effect system for atomicity", series= "ACM SIG{\-}PLAN Notices", volume = "38", issue = "5", pages = "338--349", month = may, year = "2003", publisher = "ACM Press", booktitle="Proceedings of PLDI'03" } @InProceedings{FP91:pldi, author = "T. Freeman and F. Pfenning", title = "Refinement Types for {ML}", booktitle= "Proceedings of PLDI'91", publisher= "ACM Press", year = 1991, pages = "268--277"} @InProceedings{HMcA97:pldi, title={Linear-time Subtransitive Control Flow Analysis}, author={N. Heintze and D. A. McAllester}, booktitle={Proceedings of PLDI'97}, pages={261--272}, publisher= "ACM Press"} @InProceedings{PE88:pldi, author = "F. Pfenning and C. Elliott", title = "Higher-Order Abstract Syntax", booktitle = "Proceedings of PLDI'88", year = "1988", pages = "199--208", publisher= "ACM Press" } @inproceedings{SF94:pldi, author = "A. Sabry and M. Felleisen", year = "1994", month = "June", booktitle = "Proc. SIGPLAN '94 Conference on Programming Language Design and Implementation", pages = "??", title = "Is Continuation-Passing Useful for Data Flow Analysis?" } @INPROCEEDINGS{SA95:pldi, Booktitle = {Proceedings of PLDI'95}, AUTHOR = {Z. Shao and A. W. Appel}, TITLE = {A Type-Based Compiler for {Standard ML}}, YEAR = 1995, publisher = "ACM Press" } @InProceedings{mor+96:pldi, author = "D. Tarditi and G. Morrisett and P. Cheng and C. Stone and R. Harper and P. Lee", title = "{TIL}: A Type-Directed Optimizing Compiler for {ML}", booktitle = "Proceedings of PLDI'96", pages = {181-192}, year={1996}, publisher = "ACM Press" } @InProceedings{NL98:pldi, author = "G.C. Necula and P. Lee", title = "{The Design and Implementation of a Certifying Compiler}", year = "1998", pages = "333--344", publisher = "ACM Press", booktitle = "Proceedings of PLDI'98"} @InProceedings{XP98:pldi, title={Eliminating Array Bound Checking Through Dependent Types}, booktitle={Proceedings of PLDI'98}, year={1998}, author={H. Xi and F. Pfenning}, publisher = "ACM Press", pages={249--257}} @inproceedings{YHR99:pldi, author = "S. H. Yong and S. Horwitz and T. Reps", title = "Pointer Analysis for Programs with Structures and Casting", journal = "ACM SIG{\-}PLAN Notices", volume = "34", number = "5", pages = "91--103", month = may, year = "1999", note={Proceedings of PLDI'99}, publisher={ACM Press}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % TYPES % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @inproceedings{thierry92:bra, author={T. Coquand}, title={Pattern Matching with Dependent Types}, booktitle={{Informal proceedings of Logical Frameworks'92}}, editor={B. Nordstr\"om and K. Pettersson and G. Plotkin}, pages={66--79}, year={1992}} @inproceedings{herman92:bra, author={H. Geuvers}, title={ Inductive and coinductive types with iteration and recursion}, booktitle={{Informal proceedings of Logical Frameworks'92}}, editor={B. Nordstr\"om and K. Pettersson and G. Plotkin}, pages={193--217}, year={1992}} @inproceedings{CS93:bra, author={T. Coquand and J. Smith}, title={The Status of Pattern Matching in Type Theory}, booktitle={Informal proceedings of {TYPES}'93}, editor={H. Geuvers}, pages={??-??}, url={http://www.dcs.ed.ac.uk/lfcsinfo/research/types-bra/proc/index.html}, year={1993}} @inproceedings{DHW93:bra, author={G. Dowek and G. Huet and B. Werner}, title={On the existence of long $\beta\eta$-normal forms in the cube}, booktitle="Informal Proceedings of TYPES'93", year = "1993", pages={115-130}, url={http://www.dcs.ed.ac.uk/lfcsinfo/research/types-bra/proc/index.html}, editor={H. Geuvers}} @InProceedings{pfe93:bra, author = "F. Pfenning", title = "Refinement Types for Logical Frameworks", booktitle = "Informal Proceedings of TYPES'93", editor = "H. Geuvers", year = "1993", pages = "285--299", url= "http://www.dcs.ed.ac.uk/lfcsinfo/research/types-bra/proc/index.html"} @inproceedings{randy90:bra, author = "R. Pollack", title = "Implicit Syntax", booktitle = "Informal Proceedings of Logical Frameworks'90, Antibes", year = "1990", month = "May", editor={G. Huet and G. Plotkin}} @inproceedings{erik97:bra, author = {E. Poll}, title = {{S}ubtyping and {I}nheritance for {I}nductive {T}ypes}, year = {1997}, booktitle = {Proceedings of TYPES'97 Workshop on Subtyping, inheritance and modular development of proofs, Durham, UK} } @inproceedings{randy92:bra, author={R. Pollack}, title={Typechecking in Pure Type Systems}, booktitle={Informal proceedings of Logical Frameworks'92}, editor={B. Nordstr\"om}, pages={271--288}, url={http://www.dcs.ed.ac.uk/lfcsinfo/research/types-bra/proc/index.html}, year={1992}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % FOOL % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @inproceedings{hen97:fool, title={Breaking through the $n^3$ barrier: Faster object type inference}, author={F. Henglein}, booktitle={Electronic proceedings of FOOL'4}, year={1997}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % ISSAC % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @inproceedings{BHC95:issac, author={C. Ballarins and K. Homann and J. Calmet}, title={Theorems and algorithms: an interface between Maple and Isabelle}, booktitle={Proceedings of ISSAC'95}, year={1995}} @inproceedings{Kaj92:issac, author={N. Kajler}, title={{CAS/PI}: a portable and extensible interface for computer algebra systems}, year={1992}, booktitle={Proceedings of ISSAC'92}, pages={376-386}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % OOPSLA % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @inproceedings{fon04:oopsla, title = "Pluggable Verification Modules: An Extensible Protection Mechanism for the {JVM}", author = "P. Fong", booktitle="Proceedings of OOPSLA'04", year = "2004", publisher = "ACM Press", pages = "404-418", } @InProceedings{FM98:oopsla, author = "S. N. Freund and J. C. Mitchell", title = "A Type System for Object Initialization in the {Java} Bytecode Language", booktitle = "Proceedings of OOPSLA '98", series = "ACM SIGPLAN Notices", volume = "33(10)", month = oct, year = "1998", publisher = "ACM Press", pages = "310--328", } @Article{loop98:oopsla, author = "B. Jacobs and J. van den Berg and M. Huisman and M. van Berkum and U. Hensel and H. Tews", title = "Reasoning about {Java} Classes", journal = "ACM SIG{\-}PLAN Notices", volume = "33", number = "10", pages = "329--340", month = oct, year = "1998", publisher = "ACM Press"} @InProceedings{VCC97:oopsla, author = "E.N. Volanschi and C. Consel and C. Cowan", title = "Declarative Specialization of Object-Oriented Programs", pages = "286--300", booktitle = "Proceedings of OOPSLA'97", month = oct, series = "ACM SIGPLAN Notices", volume = "32 (10)", publisher = "ACM Press", year = "1997" } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % OTHERS % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @inproceedings{AB05:csfw, author={A. Almeida Matos and G. Boudol}, title={On Declassification and the Non-Disclosure Policy}, pages = {226--240}, booktitle={Proceedings of {CSFW}'05}, year={2005}, publisher={IEEE Computer Society Press}} @inproceedings{AC05:csfw, author={M. Abadi and V. Cortier}, title={Deciding knowledge in security protocols under (many more) equational theories}, booktitle={Proceedings of {CSFW}'05}, year={2005}, publisher={IEEE Computer Society Press}} @inproceedings{AF03:ndss, title={Access Control based on Execution History}, author={M. Abadi and C. Fournet}, booktitle={Proceedings of NDSS'03}, pages={107--121}, year={2003}, publisher={Internet Society}} @inproceedings{BN02:csfw, title={{Secure Information Flow and Pointer Confinement in a Java-like Language}}, author={A. Banerjee and D. A. Naumann}, booktitle={Proceedings of CSFW'02}, year={2002}, publisher={IEEE Computer Society Press}} @inproceedings{BN03:csfw, title={{Using Access Control for Secure Information Flow in a Java-like Language}}, author={A. Banerjee and D. A. Naumann}, booktitle={Proceedings of CSFW'03}, year={2003}, publisher={IEEE Computer Society Press}} @inproceedings{BBF02:sac, author = "R. Barbuti and C. Bernardeschi and N. De Francesco", title = "Checking security of Java bytecode by abstract interpretation", booktitle = "Proceedings of {SAC}'02", year = "2002", pages={229-236} } @InProceedings{BR93:ccs, author = "M. Bellare and P. Rogaway", title = "Random Oracles are Practical: {A} Paradigm for Designing Efficient Protocols", pages = "62--73", booktitle = "Proceedings of the 1st {ACM} Conference on Computer and Communications Security", year = "1993", month = nov, publisher = "ACM Press"} @InProceedings{BH07:csf, author={L. Beringer and M. Hofmann}, title={Secure information flow and program logics}, booktitle={Proceedings of CSF'07}, year={2007}, publisher={IEEE Computer Society Press}} @inproceedings{BFL02:compsac, author = "C. Bernardeschi and N. De Francesco and G. Lettieri", title = "Using Standard Verifier to Check Secure Information Flow in Java ", booktitle ="Proceedings of {COMPSAC}'02", year = "2002", pages={850-855}} @InProceedings{BGJ02:ppdp, author = "F. Besson and T. Grenier de Latour and T. Jensen", title = "Secure calling contexts for stack inspection", pages = "76--87", booktitle = "Proceedings of {PPDP}'02", publisher = "ACM Press", year = "2002"} @InProceedings{centaur, author={P. Borras and D. Cl{\'e}ment and Th. Despeyroux and J. Incerpi and G. Kahn and B. Lang and V. Pascual}, title={Centaur: the system}, booktitle={Proceedings of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments}, year={1988}, publisher={ACM Press}, pages = "14--24"} @InProceedings{CGH98:stoc, author = "R. Canetti and O. Goldreich and S. Halevi", title = "The Random Oracle Methodology, Revisited", pages = "209--218", booktitle = "Proceedings of {STOC}'98", publisher = "ACM Press", address = "New York", year = "1998"} @InProceedings{CBR02:dsn, author={L. Casset and L. Burdy and A. Requet}, title={{Formal Development of an Embedded Verifier for JavaCard ByteCode}}, year={2002}, booktitle={Proceedings of DSN'02}, publisher={IEEE Computer Society}} @InProceedings{cer+99:csfw, author = "I. Cervesato and N. A. Durgin and P. D. Lincoln and J. C. Mitchell and A. Scedrov", title = "A meta-notation for protocol analysis", added-by = "gka", added-at = "Tue Mar 28 10:38:34 2000", booktitle = "12th {IEEE} Computer Security Foundations Workshop", year = "1999", month = jun, publisher = "{IEEE} Computer Society Press"} @inproceedings{che02:ppdp, booktitle = {Proceedings of {PPDP}'02}, publisher = {ACM Press}, year = {2002}, author={G. Chen}, title={Full Integration of Subtyping and if-expression}, pages={181-188}} @InProceedings{CFG02:cardis, author = "G. Chugunov and L.-{\AA}. Fredlund and D. Gurov", title = "Model Checking of Multi-Applet {JavaCard} Applications", pages = "87--96", booktitle = "Proceedings of {CARDIS}'02", publisher = "USENIX Association", year = "2002"} @InProceedings{bandera00:icse, author = {J. Corbett and M. Dwyer and J. Hatcliff and C. Pasareanu and Robby and S. Laubach and H. Zheng}, title = {{Bandera : Extracting Finite-state Models from Java Source Code}}, booktitle = {Proceedings of ICSE'00}, publisher={ACM Press}, year = {2000}, pages={439--448}} @InProceedings{bandera01:icse, title={Tool-supported Program Abstraction for Finite-state Verification}, author={M. Dwyer and J. Hatcliff and R. Joehanes and S. Laubach and C. Pasareanu and Robby and W. Visser and H. Zheng}, booktitle={Proceedings of ICSE'01}, year={2001}} @InProceedings{CBK+96:iwooos, title={Specialization Classes: An Object Framework for Specialization}, author={C. Cowan and A. Black and C. Krasik and C. Pu and J. Walpole and C. Consel and E.N. Volanschi}, booktitle={Proceedings of IWOOOS'96}, year={1996}} @inproceedings{DG00:csfw, author = "M. Dam and P. Giambiagi", title = "Confidentiality for Mobile Code: {The} Case of a Simple Payment Protocol", booktitle= "Proceedings of CSFW'00", year = "2000", publisher={IEEE Press}} @inproceedings{olivier98:fuji, author={O. Danvy}, title={Online Typed-directed Partial Evaluation}, booktitle={Proceedings of the Third Fuji International Symposium on Functional and Logic Programming}, year={1998}} @inproceedings{DS04:csfw, title={Lenient Array Operations for Practical Secure Information Flow}, author={Z. Deng and G. Smith}, booktitle={Proceedings of CSFW'04}, pages={115-124}, publisher={IEEE Press}, year={2004}} @InProceedings{EJ02:cardis, author = "M. Eluard and T. Jensen", title = "Secure Object Flow Analysis for Java Card", pages = "97--110", booktitle = "Proceedings of {CARDIS}'02", publisher = "USENIX Association", year = "2002" } @InProceedings{gir99:usc, author = {P.~Girard}, title = {Which security policy for multiapplication smart cards?}, booktitle = {Proceedings of Smartcard'99}, year = {1999}, publisher = "USENIX Association", } @InCollection{GM82:sosp, title = "Security Policies and Security Models", author = "J. Goguen and J. Meseguer", booktitle = "Proceedings of SOSP'82", year = "1982", publisher = "IEEE Computer Society Press", pages = "11--22"} @InProceedings{GJ01:csfw, author = "A. Gordon and A. Jeffrey", title = "Authenticity by typing for security protocols", pages = "145--159", booktitle = "Proceedings of {CSFW}'01", publisher = "IEEE Computer Society Press", year = "2001"} @InProceedings{HKS06:issse, author={C. Hammer and J. Krinke and G. Snelting}, title={Information Flow Control for Java Based on Path Conditions in Dependence Graphs}, booktitle={Proceedings of ISSSE'06}, pages={87-96}, year={2006}, PUBLISHER = {IEEE Computer Society Press}} @INPROCEEDINGS{HS06:csfw, TITLE = {Noninterference in the presence of non-opaque pointers}, AUTHOR = {D. Hedin and D. Sands}, BOOKTITLE = {Proceedings of {CSFW}'06}, YEAR = {2006}, PUBLISHER = {IEEE Computer Society Press}, PAGES = {255-269} } @INPROCEEDINGS{HWS06:csfw, AUTHOR = {M. Huisman and P. Worah and K. Sunesen}, TITLE = {A temporal logic characterisation of observational determinism}, booktitle = "Proceedings of {CSFW}'06", publisher = "IEEE Computer Society Press", pages="3--15", year="2006"} @InProceedings{JMT98:iccl, author = {T.~Jensen and D.~{Le M\'etayer} and T.~Thorn}, title = {{Security and Dynamic Class Loading in Java: A Formalisation}}, booktitle = {Proceedings of the 1998 IEEE International Conference on Computer Languages}, year = {1998}, pages = {4--15}} @InProceedings{JMT99:ssp, author = "T. Jensen and D. {Le M\'{e}tayer} and T. Thorn", title = "Verification of control flow based security policies", pages = "89--103", booktitle = "Proceedings of the {IEEE} Symposium on Research in Security and Privacy", year = "1999", publisher = "{IEEE} Computer Society Press" } @InProceedings{jon94:pepm, title={Dictionary-Free Overloading by Partial Evaluation}, author={M.P. Jones}, booktitle={Proceedings of PEPM'94}, pages={107--117}, year=1994, note={University of Melbourne, Australia, Department of Computer Science, Technical Report 94/9}} @InProceedings{mea99:sosp, author = "C. Meadows", title = "Analysis of the Internet Key Exchange Protocol using the {NRL} Protocol Analyzer", pages = "216--233", booktitle = "Proceedings of SOSP'99", publisher = "IEEE Computer Society Press", year = "1999", } @InProceedings{MK99:usc, author = {M.~Montgomery and K.~Krishna}, title = {{Secure Object Sharing in Java Card}}, booktitle = {Proceedings of Usenix workshop on Smart Card Technology, (Smartcard'99)}, year = {1999} } @Inproceedings{mor+99:csss, title={TALx86: A Realistic Typed Assembly Language}, booktitle={Proceedings of 1999 ACM SIGPLAN Workshop on Compiler Support for System Software}, pages={25--35}, author={G. Morrisett and K. Crary and N. Glew and D. Grossman and R. Samuels and F. Smith and D. Walker and S. Weirich and S. Zdancewic}, year={1999}, pubclisher="ACM Press"} @inproceedings{ML97:sosp, title={A Decentralized Model for Information Flow Control}, booktitle={Proceedings of SOSP'97}, year={1997}, pages={129--142}, author={A.C. Myers and B. Liskov}, publisher={ACM Press}} @InProceedings{MSZ04:csfw, author = "A.C. Myers and A. Sabelfeld and S. Zdancewic", title = "Enforcing Robust Declassification", pages = "172--186", booktitle = "Proceedings of {CSFW}'04", year = "2004", publisher = "{IEEE} Press", } @InProceedings{NL96:osdi, author = "G.C. Necula and P. Lee", title = "Safe Kernel Extensions Without Run-Time Checking", booktitle = "Proceedings of OSDI'96", year = "1996", pages={229--243}, publisher="Usenix"} @InProceedings{NCC06:csfw, title = "Information-Flow Security for Interactive Programs", author = "K. R. O'Neill and M. R. Clarkson and S. Chong", publisher = "IEEE Computer Society", year = "2006", booktitle = "Proceedings of CSFW'06", pages = "190--201" } @InProceedings{NE02:issta, author = "J.W. Nimmer and M.D. Ernst", title = "Automatic Generation of Program Specifications", pages = "232--242", booktitle = "Proceedings of ISSTA'02", series = "Software Engineering Notes", volume = "27, 4", publisher = "ACM Press", year = "2002"} @inproceedings{NE02:FSE, author = {J.W. Nimmer and M.D. Ernst}, title = {Invariant inference for static checking: An empirical evaluation}, booktitle = {Proceedings of {FSE'02}}, pages = {11--20}, year = {2002}, publisher = "ACM Press"} @InProceedings{OK99:usc, author = {M. Oestreicher and K. Krishna}, title = {{Object Lifetimes in Java Card}}, booktitle = {Proceedings of Usenix workshop on Smart Card Technology, (Smartcard'99)}, year = {1999} } @InProceedings{PW01:sosp, author = "B. Pfitzmann and M. Waidner", title = "A model for asynchronous reactive systems and its application to secure message transmission", pages = "184--201", booktitle = "Proceedings of {SOSP}'01", publisher = "IEEE Press", year = "2001"} @inproceedings{PBJ00:cardis, author = "E. Poll and J. {van den} Berg and B. Jacobs", title = {{Specification of the \mbox{JavaCard} API in JML}}, booktitle = "Proceedings of CARDIS'00", publisher = kluwer, pages = "135--154", year = "2000",} @InProceedings{pot02:csfw, author = "F. Pottier", title = "A Simple View of Type-Secure Information Flow in the pi-Calculus", booktitle = "Proceedings of {CSFW}'02", publisher="IEEE Press", year = "2002", pages={320--330}} @inproceedings{RS06:csfw, author = {A. Russo and A. Sabelfeld}, title = {Securing interaction between threads and the scheduler}, booktitle = {Proceedings of CSFW'06}, year = {2006} } @InProceedings{SS05:csfw, author = "A. Sabelfeld and D. Sands", title = " Dimensions and Principles of Declassification", booktitle = "Proceedings of {CSFW}'05", publisher="IEEE Press", year = "2005",} @inproceedings{sel91:plt, author={J. Seldin}, title={Excluded Middle and Definite Descriptions in the Theory of Constructions}, booktitle={Proceedings of the First Montreal Workshop on Programming Language Theory}, editors={M. Okada and P. Scott}, pages={74--83}, year={1991}} @InProceedings{sim02:csfw, title={{Fine-grained Information Flow Analysis for a Lambda-Calculus with Sum Types}}, booktitle={{Proceedings of CSFW'02}}, pages={223-237}, author={V. Simonet}, year={2002}} @InProceedings{smi01:csfw, title={{A New Type System for Secure Information Flow}}, pages={115-125}, booktitle={{Proceedings of CSFW'01}}, author={G. Smith}, year={2001}} @inproceedings{vol00:csfw, author = "D. Volpano", title = "Secure Introduction of One-way Functions", booktitle = "Proceedings of {CSFW}'00", pages = "246--254", year = 2000, publisher = "IEEE Press", } @InProceedings{VS97:csfw, author = "D. Volpano and G. Smith", title = "Eliminating Covert Flows with Minimum Typings", pages = "156-168", booktitle = "Proceedings of {CSFW}'97", publisher = "IEEE Press", year = "1997"} @inproceedings{VS98:csfw, author = "D. Volpano and G. Smith", title = "Probabilistic Noninterference in a Concurrent Language", booktitle = "Proceedings of {CSFW}'98", publisher = "IEEE Press", pages = "34--43", year = 1998 } @inproceedings{tai75:lc, author={W. Tait}, title={A realisability interpretation of the theory of species}, booktitle={Logic Colloquium 73}, editor={R. Parikh}, pages={240--251}, series=lnm, volume={453}, year={1975}} @InProceedings{RW91:iclp, author = "E. J. Rollins and J. M. Wing", title = "Specifications as Search Keys for Software Libraries", pages = "173--187", editor = "K. Furukawa", booktitle = "Proceedings of {ICLP}'91", month = jun, year = "1991", publisher = "MIT Press"} @InProceedings{WF98:sosp, author = "D.S. Wallach and E.W. Felten", title = "Understanding Java Stack Inspection", pages = "52--65", booktitle = "Proceedings of SOSP'98", publisher = "IEEE Press", year = "1998", } @inproceedings{zan91:csn, author={H. Zantema}, title={Termination of term-rewriting: from many-sorted to one-sorted}, booktitle={Proceedings of CSN'91}, pages={617-629}, editor={J. van Leeuwen}, year={1991}, note={Also appeared as report RUU-CS-91-18, University of Utrecht}} @InProceedings{ZM01:csfw, author = "S. Zdancewic and A.C. Myers", title = "Robust Declassification", pages = "15--23", booktitle = "Proceedings of {CSFW}'01", year = "2001", publisher = "{IEEE} Press", } @inproceedings{ZM03:csfw, author={S. Zdancewic and A.C. Myers}, title={Observational Determinism for Concurrent Program Security}, booktitle={Proceedings of {CSFW}'03}, publisher={IEEE Press}, pages={29-46}, year={2003}} @InProceedings{sin72:paap, author = {M. Sintzoff}, title = {Calculating properties of programs by valuations on specific models}, booktitle = {Proceedings of the ACM conference on proving assertions about programs}, pages = {203--207}, year = {1972}, volume = {SIGPLAN Notices vol 7, No 1, SIGACT News N0 14}, } @INPROCEEDINGS {RCG04:pppj, AUTHOR = {C. Rippert and A. Courbot and G. Grimaud}, TITLE = {{A Low-Footprint Class Loading Mechanism for Embedded Java Virtual Machines}}, BOOKTITLE = {Proceedings of PPPJ'04}, YEAR = {2004}, pubisher={ACM Press} } @inproceedings{ springintveld96thirdorder, author = "J. G.~Springintveld", title = "Third-order matching in the polymorphic lambda calculus", booktitle = "Proceedings of the Second International Workshop on Higher-Order Algebra, Logic, and Term Rewriting ({HOA} '95)", volume = "1074", publisher = "Springer-Verlag", editor = "G.~Dowek and J.~Heering and K.~Meinke and B.~M{\"o}ller", pages = "221--238", year = "1996", url = "citeseer.ist.psu.edu/springintveld95thirdorder.html" }