@STRING{tlca1 ={Proceedings of {TLCA}'93}} @STRING{tlca2 ={Proceedings of {TLCA}'95}} @STRING{tlca3 ={Proceedings of {TLCA}'97}} @STRING{tlca3 ={Proceedings of APPSEM'00}} @InProceedings{poplmark, title = "{Mechanized Metatheory for the Masses: The PoplMark Challenge}", author = "B.E. Aydemir and A. Bohannon and M. Fairbairn and J.N. Foster and B.C. Pierce and P. Sewell and D. Vytiniotis and G. Washburn and S. Weirich and S. Zdancewic", year = "2005", booktitle = "Proceedings of TPHOLs'05", pages = "50--65", EDITOR = {J. Hurd and T. Melham}, PUBLISHER = springer, SERIES = lncs, VOLUME = 3603} @inproceedings{qed, AUTHOR="\mbox{}", TITLE="The {QED} manifesto", BOOKTITLE="Proceedings of CADE-12", EDITOR="A.Bundy", PAGES="238--251", PUBLISHER="Springer-Verlag", YEAR=1994, MONTH="June/July", NOTE="lnai 814"} @inproceedings{abe99:types, author={A. Abel}, title={On Relating Type Theories and Set Theories}, booktitle={Proceedings of {TYPES}'99}, editor = {T. Coquand and P. Dybjer and B. Nordstr{\"o}m and J. Smith}, publisher = springer, series = lncs, volume = {1956}, year = {2000}, pages={1-20}} @inproceedings{petera98:types, author={P. Aczel}, title={{On Relating Type Theories and Set Theories}}, pages={1--18}, booktitle={{Proceedings of {TYPES}'98}}, editor={T. Altenkirch and W. Naraschewski and B. Reus}, Publisher=springer, series= lncs, year={1999}, volume= {1657}} @InProceedings{AF97:fme, author = "S. Agerholm and J. Frost", title = "Towards an Integrated {CASE} and Theorem Proving Tool for {VDM}-{SL}", booktitle = "Proceedings of FME'97", editor = "J. Fitzgerald and C.B. Jones and P. Lucas", volume = "1313", series = lncs, publisher = springer, year = "1997", pages = "278--297" } @Inproceedings{age95:ecoop, author = "O. Agesen", title = "The Cartesian Product Algorithm: Simple and Precise Typing of Parametric Polymorphism", series = lncs, publisher = springer, editor = "W. Olthoff", volume = "952", booktitle= "Proceedings of ECOOP'95", year = "1995", pages = "2--26" } @inproceedings{thorsten98:csl, author={T. Altenkirch}, title={Logical relations and inductive/coinductive types}, year={1998}, Booktitle={Proceedings of {CSL}'98}, editor={G. Gottlob, E. Grandjean and K. Seyr}, pages={343--354}, Publisher=springer, series= lncs, volume= {1584}} @inproceedings{thorsten01:tlca, author={T. Altenkirch}, title={Representations of First Order Function Types as Terminal Coalgebras}, booktitle={Proceedings of {TLCA}'01}, pages={8--21}, volume = {2044}, year = {2001}, editor={S. Abramsky}, series=lncs, publisher=springer} @inproceedings{tt01:tlca, author={T. Altenkirch and T. Coquand}, title={A Finitary Subsystem of the Polymorphic Lambda-Calculus}, booktitle={Proceedings of {TLCA}'01}, pages={22--28}, volume = {2044}, year = {2001}, editor={S. Abramsky}, series=lncs, publisher=springer} @inproceedings{AC98:fossacs, author = "R. Amadio and S. Coupet-Grimal", TITLE = "Analysis of a Guard Condition in Type Theory", EDITOR = "M. Nivat", BOOKTITLE = "Proceedings of FOSSACS'98", SERIES = lncs, VOLUME = 1378, PAGES = "48--62", PUBLISHER = springer, YEAR = 1998 } @InProceedings{ADZ04:concur, author = {Amadio, R. and {Dal Zilio}, S.}, title = {{Resource Control for Synchronous Cooperative Threads}}, booktitle = {Proceedings of CONCUR'04}, series = lncs, volume = {3170}, publisher = springer, pages = {68--82}, month = aug, year = 2004, editor={P.~Gardner and N.~Yoshida}} @inproceedings{ACL03:tphols, author={J. Andronick and B. Chetali and O. Ly}, title={{Using Coq to Verify Java Card Applet Isolation Properties}}, pages={335 - 351}, booktitle={Proceedings of {TPHOL}s'03}, editor={D. Basin and B. Wolff}, volume=2758, year={2003}, series=lncs, publisher=springer} @INPROCEEDINGS{arb96:clm, author={F. Arbab}, title={The {IWIM} model for coordination of concurrent activities}, BOOKTITLE={Coordination Languages and Models}, SERIES=lncs, volume={1061}, pages={34--56}, year={1996}, editor={P. Ciancarini and C. Hankin}} @inproceedings{AS05:esorics, title="Security-typed languages for implementation of cryptographic protocols: A case study", booktitle="Proceedings of ESORICS'05", year="2005", editor="S. De Capitani di Vimercati and P.F. Syverson and D. Gollmann", publisher=springer, series=lncs, volume=3679, pages="197-221", author="A. Askarov and A. Sabelfeld"} @InProceedings{asp94:csl, author = "D. Aspinall", title = "Subtyping with Singleton Types", booktitle = "Proceedings of {CSL}'94", pages = "1--15", year = "1994", publisher = springer, series=lncs, volume={933}, editor={L. Pacholski and J. Tiuryn}} @inproceedings{AH02:esop, author = "D. Aspinall and M. Hofmann", title = "Another Type System for In-Place Update", series=lncs, booktitle="Proceedings of ESOP'02", volume = "2305", pages = "36--52", year = "2002", editor={D. Le M\'etayer}} @inproceedings{asp+04:cassis, author={D. Aspinall and S. Gilmore and M. Hofmann and D. Sannella and I. Stark}, title={{Mobile Resource Guarantees for Smart Devices}}, series=lncs, booktitle="Proceedings of CASSIS'04", volume = "3362", pages = "1--27", year = "2005", editor={G. Barthe and L. Burdy and M. Huisman and J.-L. Lanet and T. Muntean} } @InProceedings{BPW03:esorics, author = "M. Backes and B. Pfitzmann and M. Waidner", title = "Symmetric Authentication Within a Simulatable Cryptographic Library", booktitle = "Proceedings of {ESORICS}'03", year = "2003", publisher = springer, series = lncs, pages={162-180}, editor={E. Snekkenes and D. Gollmann}, volume={2808}} @Inproceedings{BJJM98:afp, author = "R. Backhouse and P. Jansson and J. Jeuring and L. Meertens", title = "Generic Programming---An Introduction", editor = "S. D. Swierstra and P. R. Henriques and J. N. Oliveira", booktitle = "Proceedings of AFP'98", series = lncs, volume = "1608", pages = "28--115", publisher = springer, year = "1999"} @inproceedings{BBK87:rta, author={J. Baeten and J. Bergstra and J.W. Klop}, title={Priority rewrite systems}, pages={83-94}, editor={P. Lescanne}, series=lncs, volume={256}, publisher=springer, booktitle={Rewriting techniques and applications}, year={1987}} @inproceedings{anthony96:types, author = "A. Bailey", title = "Coercion Synthesis in Computer Implementations of Type-Theoretic Frameworks", booktitle={Proceedings of {TYPES}'96}, series=lncs, publisher=springer, volume = "1512", pages = "9--27", year = "1998", editor={E. Gim{\'e}nez and C. Paulin-Mohring}} @InProceedings{bak94:lfcs, author = " Bakel, S. van and L. Liquori and S. Ronchi della Roncha and P. Urzyczyn", title = "Comparing Cubes", booktitle = "Proceedings of LFCS'94", year = {1994}, editor= {A. Nerode and Y.N. Matiyasevich}, volume = {813}, series = lncs, pages = "353-365", publisher = springer, crossrefonly={lfcs94}} @inproceedings{BB00:tphols, author = "A. Balaa and Y. Bertot", title = "Fix-Point Equations for Well-Founded Recursion in Type Theory", editor = "M. Aagaard and J. Harrison", booktitle = "Proceedings of {TPHOLs}'00", series = lncs, volume = "1689", pages = "1--16", publisher = springer, year = "2000" } @InProceedings{BN04:cassis, title = "History-Based Access Control and Secure Information Flow", author = "A. Banerjee and D.A. Naumann", year = "2004", pages = "27--48", editor="G. Barthe and L. Burdy and M. Huisman and J.-L. Lanet and T. Muntean", volume=3362, series = lncs, publisher = springer, booktitle="Proceedings of CASSIS'04"} @inproceedings{BF93:tlca, author={F. Barbanera and M. Fern{\'a}ndez}, title={Combining first and higher order rewrite systems with type assignment systems}, booktitle={Proceedings of {TLCA}'93}, editor={M.Bezem and J.F. Groote}, pages={60-74}, crossref={tlca} ,year={1993}} @InProceedings{BF93:icalp, author = "F. Barbanera and M. Fern{\'a}ndez", title = "Modularity of termination and confluence in combinations of rewrite systems with {$\lambda_\omega$}", series = lncs, booktitle = "Proceedings of ICALP'93", year = "1993", pages={657--668}, editor={A. Lingas and R. Karlsson and S. Karlsson}, volume={700}, publisher =springer} @inproceedings{BH90:esop, author={H. Barendregt and K. Hemerik}, title={Types in lambda calculi and programming languages}, booktitle={Proceedings of ESOP'90}, editor={N. Jones}, pages={1--36}, series=lncs, volume={432}, year={1990}} @inproceedings{BLS04:cassis, title={{The Spec\# Programming System: An Overview}}, author={M. Barnett and K.R.M. Leino and W. Schulte}, booktitle={Proceedings of {CASSIS}'04}, series=lncs, publisher=springer, volume={3362}, year={2005}, pages={50--71}, editor={G. Barthe and L. Burdy and M. Huisman and J.-L. Lanet and T. Muntean}} @inproceedings{bas+02:tphols, author={D. Basin and S. Friedrich and M. Gawkowski}, title={Verified Bytecode Model Checkers}, series=lncs, publisher=springer, volume={2410}, year={2002}, booktitle={Proceedings of {TPHOLs}'02}, pages={47-66}, editor={V. Carre{\~n}o and C. Mu{\~n}oz and S. Tahar}} @InProceedings{BCK05:icalp, author = "M. Baudet and V. Cortier and S. Kremer", booktitle = "{P}roceedings of {ICALP}'05", note = "To appear", publisher = springer, series = lncs, title = "Computationally Sound Implementations of Equational Theories against Passive Adversaries", year = "2005"} @InProceedings{BLS96:cav, author = "S. Bensalem and Y. Lakhnech and H. Saidi", booktitle = "Proceedings of CAV'96", editor = "R. Alur and T.A. Henzinger", pages = "323--335", publisher = "Springer Verlag", series = lncs, title = "Powerful Techniques for the automatic Generation of Invariants", volume = "1102", year = "1996"} @inproceedings{randyetal93:bra, author={Benthem Jutting, L.S. van and McKinna, J. and Pollack, R.}, title={Checking algorithms for pure type systems}, pages={19-61}, series=lncs, publisher=springer, volume={806}, year={1994}, booktitle={Proceedings of {TYPES}'93}, crossref={types93}} @InProceedings{BBC95:tlca , Author ={S. Berardi and M. Bezem and T. Coquand} , Title={A realization of the negative interpretation of the Axiom of Choice} , Booktitle={Proceedings of {TLCA}'95} , Year= 1995 , Publisher= springer , series= lncs , volume= {902} , pages={47--62} , Editor= {M. Dezani-Ciancaglini and G. Plotkin} , crossref={tlca95}} @InProceedings{vdBJ01:tacas, author = "Berg, J. van den and Jacobs, B.", title = "{The LOOP Compiler for Java and JML}", booktitle = "{Proceedings of TACAS'01}", series=lncs, volume=2031, pages={299--312}, editor={T. Margaria and W. Yi}, year={2001}} @INPROCEEDINGS{BJP01:esmart, AUTHOR = "Berg, J. van den and B. Jacobs and E. Poll", TITLE = {{Formal Specification and Verification of JavaCard's Application Identifier Class}}, EDITOR = {I. Attali and T. Jensen}, BOOKTITLE = {Proceedings of e-{SMART}'00}, SERIES = lncs, VOLUME = {2041}, PAGES = {137--150}, PUBLISHER = {Springer Verlag}, YEAR = 2001 } @InProceedings{BS94:lcc, author = "U. Berger and H. Schwichtenberg", title = "Program Extraction from Classical Proofs", pages = "77--97", editor = "D. Leivant", booktitle = "Proceedings of {LCC}'94", series = lncs, volume = "960", publisher = springer, year = "1995", } @InProceedings{BN00:types, author={S. Berghofer and T. Nipkow}, title={Executing Higher Order Logic}, editor={P. Callaghan and Z. Luo and J. McKinna and R. Pollack}, booktitle={Proceedings of {TYPES}'00}, publisher=springer, volume={2277}, year={2002}, series=lncs, pages={24--40}} @inproceedings{BdF02:vmcai, title={{Combining Abstract Interpretation and Model Checking for analysing Security Properties of Java Bytecode}}, author={C. Bernardeschi and N. De Francesco}, booktitle={Proceedings of VMCAI'02}, editor={A. Cortesi}, year={2002}, series=lncs, volume={2294}, pages={1--15}} @InProceedings{BCB02:tphols, title = "Type-Theoretic Functional Semantics", author = "Y. Bertot and V. Capretta and K. Das Barman", year = "2002", booktitle = "Proceedings of TPHOLs'02", pages = "83--98", editor={V. Carre{\~n}o and C. Mu{\~n}oz and S. Tahar}, series=lncs, Publisher=springer, volume={2410}, } @inproceedings{yves01:cav, author = {Y. Bertot}, title = {{Formalizing in Coq a type system for object initialization in the Java bytecode language}}, year = {2001}, series = lncs, booktitle ="Proceedings of CAV'01", editor={G. Berry and H. Comon and A. Finkel}, volume={2102}, pages={14--24}, Publisher= springer} @inproceedings{BGL04:types, author = {Y. Bertot and B. Gr\'egoire and X. Leroy}, editor = {J-C. Filliatre and C.~Paulin and B.~Werner}, year = {2005}, series = lncs, booktitle ="Proceedings of TYPES'04", title={A structured approach to proving compiler optimizations based on dataflow analysis}, volume={3xxx}, note={To appear}, Publisher= springer} @inproceedings{BF95:tapsoft, title = "{R}easoning with {E}xecutable {S}pecifications", author = "Y. Bertot and R. Fraer", volume = 915, pages = "531--545", editor = "P. D. Mosses and M. Nielsen and M. I. Schwartzbach", year = 1995, series = lncs, booktitle = "Proceedings of TAPSOFT'95", Publisher= springer} @inproceedings{lan+00:entcs, author = "P. Bieber and J. Cazin and V. Wiels and G. Zanon and P. Girard and J.-L. Lanet", title = "{Electronic Purse Applet Certification}", series=entcs, booktitle="Proceedings of the Workshop on Secure Architectures and Information Flow", volume = "32", publisher =elsevier, editor = "S. Schneider and P. Ryan", year = "2000" } @inproceedings{lan+00:esmart, author = "P. Bieber and J. Cazin and A. El Marouani and P. Girard and J.-L. Lanet and V. Wiels and G. Zanon", title = "The PACAP Prototype: A Tool for Detecting Java Card Illegal Flow", series=lncs, booktitle="Proceedings of {e-SMART}'00", publisher =springer, editor = "I. Attali and T. Jensen", year = "2001", volume = "2041", pages = "25--37" } @inproceedings{BM98:mpc, author = "R. Bird and L. Meertens", title = "Nested Datatypes", editor = "J. Jeuring", booktitle = "Proceedings of MPC'98", series = lncs, volume = "1422", pages = "52--67", publisher = "Springer-Verlag", year = "1998" } @InProceedings{bla05:csl, title = "Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations", author = "F. Blanqui", booktitle = "Proceedings of {CSL}'05", publisher = springer, year = "2005", volume = "3634", editor = "C.-H.L. Ong", pages = "135--150", series = lncs } DOI resolver Try KVK @inproceedings{bla04:rta, author={F. Blanqui}, title={A type-based termination criterion for dependently-typed higher-order rewrite systems}, booktitle={Proceedings of {RTA}'04}, series=lncs, volume=3091, year={2004}, editor={V. van Oostrom}, pages={24-39}} @inproceedings{BJO99:rta, author={F. Blanqui and J.-P. Jouannaud and M. Okada}, title={The algebraic Calculus of Constructions}, editor = "P. Narendran and M. Rusinowitch", pages = "301--316", series=lncs, publisher=springer, volume={1631}, year={1999}, booktitle={Proceedings of RTA'99}} @inproceedings{BR96:rta, Author = "R. Bloo and K. Rose", Title = "Combinatory Reduction Systems with Explicit Substitutions that Preserve Strong Normalisation", booktitle= "RTA '96", series =lncs, editor={H. Ganzinger}, publisher=springer, volume={1103}, Year = {1996}, } @inproceedings{BKLN02:latin, author = "R. Bloo and F. Kamareddine and T. Laan and R. Nederpelt", title = "Parameters in Pure Type Systems", booktitle={{Proceedings of LATIN'2002}}, editor={S. Rajsbaum}, volume = "2286", pages = "371--385", year = "2002"} @inproceedings{BDNN99:fossacs, title={Static Analysis of Processes for No Read-Up and No Write-Down}, author={C. Bodei and P. Degano and F. Nielson and H. R. Nielson} ,Booktitle={Proceedings of FOSSACS'99} , Year= 1999 , Publisher=springer , series= lncs , volume= {1578} , Editor= {W. Thomas} , pages={120--134}} @InProceedings{bol97:cav, author = "D. Bolignano", title = "Towards a Mechanization of Cryptographic Protocol Verification", booktitle = "Proceedings of CAV'97", year = "1997", editor={O. Grumberg}, Publisher=springer, series= lncs, volume=1254, pages={131--142} } @InProceedings{bol98:cav, author = "D. Bolignano", year = "1998", title = "Integrating Proof-Based and Model-Checking Techniques for the Formal Verification of Cryptographic Protocols", booktitle = "Proceedings of CAV'98", series=lncs, volume = "1427", pages = "77--87"} @InProceedings{BCM05:cassis, title = "Information Flow Analysis for a Typed Assembly Language with Polymorphic Stacks", author = "E.~Bonelli and A.B.~Compagnoni and R.~Medel", publisher = springer, year = "2005", volume = "3956", booktitle = "Proceedings of CASSIS'05", editor = "G.~Barthe and B.~Gr{\'e}goire and M.~Huisman and J.-L. Lanet", pages = "37--56", series = lncs } @inproceedings{BS99:fssj, author= {E. B\"orger and W. Schulte}, title="A {P}rogrammer {F}riendly {M}odular {D}efinition of the {S}emantics of {J}ava", booktitle="Formal Syntax and Semantics of Java", publisher=springer, series=lncs, volume= 1523, year=1999, editor={J. Alves-Foss}, pages={353--404} } @inproceedings{bou04:esop, author={G. Boudol}, title={{ ULM: A Core Programming Model for Global Computing: (Extended Abstract).W}}, booktitle= "Proceedings of ESOP'04", pages={234--248}, publisher=springer, series=lncs, volume=2986, editor="D.A. Schmidt", year=2004} @inproceedings{BC01:icalp, author = "G. Boudol and I. Castellani", title = "Noninterference for Concurrent Programs", series=lncs, volume = "2076", pages = "382--395", year = "2001", booktitle="Proceedings of ICALP'01", editor="F. Orejas and P.G. Spirakis and J. van Leeuwen" } @inproceedings{samuel97:tacs, author = "S. Boutin", title = "Using Reflection to Build Efficient and Certified Decision Procedures", booktitle = "Proceedings of TACS'97", year = {1997}, editor={M. Abadi and T. Ito}, series =lncs, publisher = springer, volume = 1281, pages = "515--529" } @inproceedings{BC01:tphols, author = "A. Bove and V. Capretta", title = "Nested General Recursion and Partiality in Type Theory", editor = "R. J. Boulton and P. B. Jackson", booktitle = "Proceedigns of {TPHOLs}'01", series = lncs, volume = 2152, year = 2001, publisher = springer, pages = "121--135" } @inproceedings{BJB02:amast, title = {{Specifying and Verifying a Decimal Representation in Java for Smart Cards}}, author = "C. Breunesse and B. Jacobs and Berg, J. van den", year = 2002, booktitle ="Proceedings of AMAST'02", publisher = springer, pages = "304--318", series = lncs, volume = 2422, editor = "H. Kirchner and C. Ringeissen" } @Book{buc+81, author = "W. Buchholz and S. Feferman and W. Pohlers and W. Sieg", title = "Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Results", series = lnm, volume = "897", publisher = springer, year = "1981", } @inproceedings{BRL03:fme, title = {{Java Applet Correctness: a Developer-Oriented Approach}}, author = "L. Burdy and A. Requet and J.-L. Lanet", year = 2003, booktitle = "Proceedings of FME'03", publisher = springer, series = lncs, volume = 2805, pages = "422--439", editor="K. Araki and S. Gnesi and D. Mandrioli"} @inproceedings{BMcK:del, title = "Deliverables: An Approach to Program Development in the Calculus of Constructions", author = "R. Burstall and J. McKinna", booktitle = "Proceedings of MFCS'93", editor = {A.M. Borzyszkowski and S. Sokolowski}, series=lncs, volume={711}, publisher=springer, pages = {32--67}, year = 1993} @INPROCEEDINGS{CP03:tphols, AUTHOR = {D. Cachera and D. Pichardie}, TITLE = {{Embedding of Systems of Affine Recurrence Equations in Coq}}, BOOKTITLE = {Proceedings ofTPHOLs'03}, YEAR = {2003}, PAGES = {155--170}, NUMBER = {2758}, SERIES = lncs, PUBLISHER =springer, editors="" } @INPROCEEDINGS{cac+05:fm, AUTHOR = {D. Cachera and T. Jensen and D. Pichardie and G. Schneider}, TITLE = {{Certified Memory Usage Analysis}}, BOOKTITLE ={{Proceedings of FM'05}}, YEAR = {2005}, editor = {J.~Fitzgerald and I.~Hayes and A.~Tarlecki}, series=lncs, pages="91--106", volume={3582}, publisher=springer} @InProceedings{cas02:fme, author={L. Casset}, title={{Development of an Embedded Verifier for JavaCard ByteCode using Formal Methods}}, year={2002}, booktitle={Proceedings of FME'02}, series=lncs, editor={L.-H. Eriksson and P. A. Lindsay}, volume={2391}, pages={290-309}} @inproceedings{CH02:fme, title = {Formal Specification and Static Checking of {Gemplus's} Electronic Purse Using {ESC/Java}}, author = "N. Cata{\~n}o and M. Huisman", year = 2002, booktitle = "Proceedings of FME'02", editor = "L.-H. Eriksson and P.A. Lindsay", series = lncs, publisher = springer, volume = "2391", pages = "272--289" } @inproceedings{CH03:vmcai, title = "{Chase: a Static Checker for {JML}'s Assignable Clause}", author = "N. Cata{\~n}o and M. Huisman", year = 2003, booktitle = "Proceedings of VMCAI'03", editor = "L.D. Zuck and P.C. Attie and A. Cortesi and S. Mukhopadhyay", series = lncs, volume = 2575, pages = "26--40", publisher = springer } @inproceedings{cha+05:esop, title={{Enforcing Resource Bounds via Static Verification of Dynamic Checks}}, author={A. Chander and D. Espinosa and N. Islam and P. Lee and G. Necula}, booktitle={Proceedings of ESOP'05}, year={2005}, editor={S.~Sagiv}, series=lncs, publisher=springer, volume=3444, pages={311-325}} @InProceedings{CdG99:types, author = {A.~Ciaffaglione and P.~Di Gianantonio}, title = {{A Coinductive Approach to Real Numbers}}, booktitle = {{Proceedings of {TYPES}'99}}, year = {2000}, series = lncs, volume = {1956}, editor = {Th.~Coquand and P.~Dybjer and B.~Nordstr\"om and J.~Smith}, pages = {114-130}, publisher = springer } @inproceedings{cap99:tphol, author={V. Capretta}, title ={Universal Algebra in Type Theory}, booktitle={Proceedings of {TPHOLs}'99}, year = {1999}, editor = {Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Th{\'e}ry}, volume = {1690}, series = lncs, pages={131--148}, publisher=springer} @inproceedings{cap00:tphol, author={V. Capretta}, title={Recursive families of inductive types}, pages={73--89} ,Booktitle={Proceedings of {TPHOLs}'00} , Year= 2000 , Publisher= springer , series= lncs , volume= {1869} , Editor= {M. Aagard and J. Harrison}} @InProceedings{CMMS91:tacs, title = "An Extension of system~{$F$} with Subtyping", author = "L. Cardelli and S. Martini and J. Mitchell and A. Scedrov", pages = "750--770", booktitle = {Proceedings of TACS'91}, editor = "T. Ito and A. Meyer", series = lncs, volume = "526", year = "1991", publisher = springer} @inproceedings{CHS01:esmart, author = "D. Caromel and L. Henrio and B. Serpette", title = "Context Inference for Static Analysis of {Java} Card Object Sharing", series = lncs, volume = "2140", pages = "43--57", year = "2001", publisher = springer, booktitle="Proceedings of e-SMART'01", editor={I.~Attali and T.~Jensen}} } @InProceedings{CP98:cmcs, title={A Co-iterative Characterization of Synchronous Stream Functions}, author={P. Caspi and M. Pouzet}, year={1998}, booktitle={Proceedings of CMCS'98}, editor = "B. Jacobs and L. Moss and H. Reichel and J. Rutten", series = entcs, volume = "11", publisher=elsevier} @INPROCEEDINGS{JMR04:amast, AUTHOR = {B. Jacobs and C. March{\'e} and N. Rauch}, TITLE = {Formal Verification of a Commercial Smart Card Applet with Multiple Tools}, YEAR = 2004, BOOKTITLE = {Proceedings of {AMAST}'04}, SERIES = lncs, VOLUME = 3116, publisher = springer, pages={241-257}, editor={C.~Rattray and S.~Maharaj and C.~Shankland}} @InProceedings{che97:mfcs, author = {G. Chen}, title = {Subtyping Calculus of Constructions}, booktitle = {Proceedings of MFCS'97}, editor = {I. Pr{\'\i}vara and P. Ruzicka}, volume = {1295}, series = lncs, year = {1997}, publisher = springer, pages = {189-198} } @InProceedings{CH92:lncs, author = {J. Chirimar and D. J. Howe}, title = {{Implementing Constructive Real Analysis (Preliminary Report)}}, booktitle = {{Constructivity in Computer Science}}, pages = {165-178}, year = {1992}, editor = {J.P. Myers and M.J. O'Donnel}, volume = {613}, series = lncs, publisher = springer } @inproceedings{CL02:ecoop, title={{A Simple and Practical Approach to Unit Testing: The JML and JUnit Way}}, author={Y. Cheon and G. T. Leavens}, booktitle={Proceedings of ECOOP'02}, series=lncs, volume={2374}, editor={B. Magnusson}, pages={231--255}, year={2002}} @inproceedings{chr03:tphols, author={J. Chrzaszcz}, title={{Implementing Modules in the Coq System}}, pages={270 - 286}, booktitle={Proceedings of {TPHOL}s'03}, editor={D. Basin and B. Wolff}, volume=2758, year={2003}, series=lncs, publisher=springer} @inproceedings{CZ94:cade, author={E. Clarke and X. Zhao}, title={Combining Symbolic Computation and Theorem Proving: Some Problems of {Ramanujan}}, pages={758-763}, booktitle={Proceedings of Cade-12}, year={1994}, crossref={cade94}} @inproceedings{CK04:cassis, author = "D. R. Cok and J. R. Kiniry", title = "{ESC\slash Java2}: Uniting {ESC\slash Java} and {JML} --- Progress and Issues in Building and Using {ESC\slash Java2}, Including a Case Study Involving the Use of the Tool to Verify Portions of an {Internet} Voting Tally System", volume = "3362", pages = "108--128", year = "2005", booktitle={Proceedings of {CASSIS}'04}, series=lncs, publisher=springer, editor={G. Barthe and L. Burdy and M. Huisman and J.-L. Lanet and T. Muntean} } @inproceedings (adriana94:csl, author = "A. Compagnoni" , title = "Decidability of Higher-Order Subtyping with Intersection Types", booktitle= "Proceedings of {CSL}'94" , publisher = springer , year = "1995", pages={46--60}, editor={L. Pacholski and J. Tiuryn}, series = LNCS, volume = "933" ) @inproceedings{CG99:csl, author = "A. Compagnoni and H. Goguen", title = "Anti-Symmetry of Higher-Order Subtyping", year = "1999", booktitle={Proceedings of {{CSL}}'99}, editor={J. Flum and M. Rodr{\'\i}guez-Artalejo}, volume={1683}, pages={420--438}} @inproceedings{thierry93:bra, author={T. Coquand}, title={Infinite objects type theory}, year={1994}, pages={62--78}, booktitle={Proceedings of Types'93}, series=lncs, volume={806}, publisher=springer, editor={H. Barendregt and T. Nipkow}} @inproceedings{CD94:fsttcs, author={T. Coquand and P. Dybjer}, title={Inductive definitions and type theory: an introduction (Preliminary Version)}, year={1994}, pages={60--76}, booktitle={Proceedings of FSTTCS'94}, series=lncs, volume={880}, publisher=springer, editor={P.S. Thiagarajan}} @INPROCEEDINGS{CP88:colog, AUTHOR = "T. Coquand and C. Paulin", TITLE = "Inductively defined types", BOOKTITLE = "Proceedings of {COLOG'88}", EDITOR = "P. Martin-{L}{\"o}f and G. Mints", YEAR = "1988", PUBLISHER = springer, SERIES = lncs, PAGES = "50--66", volume = "417"} @InProceedings{CT95:types, author = "C. Cornes and D. Terrasse", title = "Automating Inversion and Inductive Predicates in {Coq}", pages = "85--104", booktitle = "Proceedings of Types'95", year = "1995", publisher = springer, series=lncs, volume=1158, editor={S. Berardi and M. Coppo}} @inproceedings{CW05:esop, author={V. Cortier and B. Warinschi}, title={Computationally Sound, Automated Proofs for Security Protocols}, booktitle={Proceedings of {ESOP}'05}, series=lncs, volume=3444, publisher=springer, editor={S. Sagiv}, pages={157-171}, year=2005} @inproceedings{CGJ99:tphol, title={Hardware Verification Using Co-induction in COQ}, author={S. Coupet-Grimal and L. Jakubiec}, booktitle={Proceedings of {TPHOLs}'99}, editor={Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Th{\'e}ry}, YEAR = "1999", PUBLISHER = springer, SERIES = lncs, PAGES = "73--90", volume = "1690"} @inproceedings{cou97:tlca, AUTHOR = {Courant, J.} , TITLE = {A module calculus for {P}ure {T}ype {S}ystems} , YEAR = 1997 , volume={1210} , editor ={P. de Groote and J. Hindley} , booktitle=tlca3 , publisher =springer, series=lncs} @inproceedings{cou00:lncs2k, author = {Cousot, P.}, title = {{Abstract Interpretation Based Formal Methods and Future Challenges}}, booktitle = {Informatics --- 10 Years Back, 10 Years Ahead}, editor = {Wilhelm, R.}, year = {2001}, series = lncs, volume = 2000, pages = {138--156}, publisher = springer, } @InProceedings{CKT95:tlca , Author ={Y. Coscoy and G. Kahn and L. Th{\'e}ry.} , Title={Extracting text from proofs} , Booktitle={Proceedings of {TLCA}'95} , Year= 1995 , Publisher= springer , series= lncs , volume= {902} , pages={109--123} , Editor= {M. Dezani-Ciancaglini and G. Plotkin} , crossref={tlca95}} @inproceedings{cra00:tic, author = "K. Crary", title = "Sound and Complete Elimination of Singleton Kinds", series = lncs, volume = "2071", pages = "1--26", year = "2001", editor={R. Harper}, booktitle={Proceedings of TIC'00}, Publisher=springer} @inproceedings{CM99:icalp, author = "K. Crary and G. Morrisett", title = "Type Structure for Low-Level Programming Languages", series = lncs, volume = "1644", pages = "40--54", year = "1999", booktitle={{Proceedings of ICALP'99}}, editor={J. Wiedermann and P. van Emde Boas and M. Nielsen}} @InProceedings{DHS05:spc, author = "\'{A}. Darvas and R. H{\"{a}}hnle and D. Sands", title = "A Theorem Proving Approach to Analysis of Secure Information Flow", booktitle = "Proceedings International Conference on Security in Pervasive Computing", pages = "193--209", year = "2005", editor = "D. Hutter and M. Ullmann", volume = "3450", series = lncs, publisher = springer, note="Preliminary version in the informal proceedings of WITS'03" } @InProceedings{del00:lpar , Author ={D. Delahaye} , Title={{A Tactic Language for the System Coq}} ,Booktitle={Proceedings of {LPAR}'00} , Year= 2000 , Publisher=springer , series= lncs , volume= {1955} , Editor= {M. Parigot and A. Voronkov} , pages={85--95}} @inproceedings{DM02:wrla, title={Modeling Group Communication Protocols Using Multiset Term Rewriting}, author={G. Denker and J. Millen}, booktitle={Proceedings of WRLA '02}, series=entcs, volume={}} @inproceedings{DJ00:esop, author={E. Denney and T. Jensen}, title={{Correctness of Java Card method lookup via logical relations}}, booktitle={Proceedings of ESOP'00}, pages={104--118}, editor={G. Smolka}, series= lncs, PUBLISHER=springer, year={2000}, volume={1782}} @inproceedings{den02:asiacrypt, author={A. W. Dent}, title={{Adapting the Weaknesses of the Random Oracle Model to the Generic Group Model}}, booktitle="Proceedings of ASIACRYPT'02", year=2002, pages={100-109}, series=lncs, publisher=springer, volume=2501, editor={Y. Zheng}} @inproceedings{Der93:tr, author={N. Dershowitz}, title={33 examples of termination}, booktitle={Term rewriting}, pages={16-26}, crossref={CJ93}, editor={H. Comon and J.-P. Jouannaud}, series= lncs, PUBLISHER=springer, year={1993}, volume={909}} @InProceedings{DCG97:icalp, title={On Modular Properties of Higher Order Extensional Lambda Calculi}, author={R. Di Cosmo and N. Ghani}, pages={237--247}, editor={P. Degano and R. Gorrieri and A. Marchetti-Spaccamela}, booktitle={Proceedings of ICALP'97}, year=1997, series=lncs, volume=1256, publisher=springer } @inproceedings{DCK93:icalp, author = "Di Cosmo, R. and D. Kesner", title = "A confluent reduction for the extensional typed $\lambda-$calculus with pairs, sums, recursion and terminal object", pages={645--656}, booktitle = "Proceedings of ICALP'93", year = "1993", editor={A. Lingas and R. Karlsson and S. Karlsson}, volume={700}, publisher= springer} @InProceedings{DCP95:tlca , Author ={R. Di Cosmo and G. Piperno} , Title={Expanding extensional polymorphism} , Booktitle={Proceedings of {TLCA}'95} , Year= 1995 , Publisher= springer , series= lncs , volume= {902} , pages={?} , Editor= {M. Dezani-Ciancaglini and G. Plotkin} , month={April} , crossref={tlca95}} @inproceedings{DMPH04:cassis, author = {Dietl, W. and M\"{u}ller, P. and Poetzsch-Heffter, A.}, title = {A Type System for Checking Applet Isolation in {J}ava {C}ard}, booktitle = {Proceedings of {CASSIS}'04}, year = {2005}, pages = {129--150}, editor = {G. Barthe and L. Burdy and M. Huisman and J.-L. Lanet and T. Muntean}, volume = {3362}, series = lncs, publisher = springer } @inproceedings{dow91:mfcs, title = "A Second-Order Pattern Matching Algorithm for the Cube of Typed Lambda-Calculi", author = "G. Dowek", booktitle = "Proceedings of MFCS'91", editor = {A. Tarlecki}, series=lncs, volume={520}, publisher=springer, pages = {151--160}, year = 1991} @INPROCEEDINGS{dow93:tlca , AUTHOR = {G. Dowek} , TITLE = {The undecidability of typability in the {Lambda-Pi-Calculus}} , BOOKTITLE = tlca1 , EDITOR = {M. Bezem and J.F. Groote} , SERIES = lncs , VOLUME = 664 , PUBLISHER = springer , YEAR = 1993 , CROSSREF = {tlca} , PAGES = {139--145} } @Inproceedings{DE99:fssj, author = "S. Drossopoulou and S. Eisenbach", title = "Describing the Semantics of {Java} and {P}roving {T}ype {S}oundness", booktitle="Formal Syntax and Semantics of Java", publisher=springer, series=lncs, volume= 1523, year=1999, editor={J. Alves-Foss}, pages={41--82} } @InProceedings{DFM05:cade, title = "Privacy-Sensitive Information Flow with {JML}", author = "G. Dufay and A.P. Felty and S. Matwin", booktitle = "Proceedings of {CADE}'05", publisher = springer, year = "2005", volume = "3632", editor = "R.~Nieuwenhuis", ISBN = "3-540-28005-7", pages = "116--130", series =lncs} @inproceedings (FM94:csl, author = "M. Fairtlough and M. Mendler" , title = "An intuitionistic modal logic with applications to the formal verification of hardware", booktitle= "Proceedings of {CSL}'94" , publisher = springer , year = "1995", pages={}, editor={L. Pacholski and J. Tiuryn}, series = LNCS, volume = "933" ) @InProceedings{FH94:lpar, author = "A. Felty and D. Howe", title = "Generalization and Reuse of Tactic Proofs", pages = "1--15", editor = "F. Pfenning", booktitle = "Proceedings of {LPAR}'94", series = lnai, volume = "822", publisher = springer, year = "1994" } @inproceedings{FJ94:adt, author={M. Fern{\'a}ndez and J.-P.Jouannaud}, title={Modularity of termination of term-rewriting systems revisited}, pages={255-272}, booktitle={Recent Trends in Data Type Specification}, editor={E. Artesiano and G. Reggio and A. Tarlecki}, year={1994}, series=lncs, volume={906}, publisher=springer} @Conference{FS86:crypto, key = "FS86", author = "A. Fiat and A. Shamir", title = "{How to Prove Yourself: Practical Solutions to Identification and Signature Problems}", booktitle = "Proc. CRYPTO'86", pages = "186--194", year = "1986", publisher = springer, series = lncs, volume=286} @inproceedings{FM94:tacs, author={K. Fischer and J. Mitchell}, title={Notes on typed object-oriented programming}, booktitle={Proceedings of TACS'94}, year={1994}, editor={M. Hagiya and J. Mitchell}, series=lncs, pages={844-885}, volume={789}, publisher=springer} @inproceedings{FA99:esop, author = "C. Flanagan and M. Abadi", title = "Types for Safe Locking", series= lncs, volume = "1576", pages = "91--108", year = "1999", booktitle="Proceedings of ESOP'99", editor="D. Swiestra" } @inproceedings{FFQ02:esop, author = "C. Flanagan and S.N. Freund and S. Qadeer", title = "Thread-Modular Verification for Shared-Memory Programs", series = lncs, volume = "2305", pages = "262--277", year = "2002", editor="D. Le M{\'e}tayer", booktitle="Proceedings of ESOP'02"} @inproceedings{FL01:fme, author = "C. Flanagan and K. R. M. Leino", title = "{Houdini}, an Annotation Assistant for {ESC\slash Java}", series = lncs, volume = "2021", pages = "500--517", year = "2001", booktitle={Proceedings of FME'01}, editor={J.N. Oliveira and P. Zave}} @inproceedings{FG00:fosad, booktitle = "Foundations of Security Analysis and Design", volume = "2171", year = "2001", editor = "R. Focardi and R. Gorrieri", author= "R. Focardi and R. Gorrieri", publisher = springer, series = lncs, title={Classification of Security Properties: (Part I: Information Flow)}, pages={331--396}} @inproceedings{FRS05:fossacs, booktitle = "Proceedings of FOSSACS'05", volume = "3441", year = "2005", editor = "V. Sassone", author= "R. Focardi and S. Rossi and A. Sabelfeld", publisher = springer, series = lncs, title={{Bridging Language-Based and Process Calculi Security}}, pages={299--315}} @inproceedings{GR97:tacs, author = "J. Garrigue and D. R{\'e}my", title = "Extending {ML} with Semi-Explicit Higher-Order Polymorphism", booktitle = "Proceedings of TACS'97", year = {1997}, editor={M. Abadi and T. Ito}, series =lncs, publisher = springer, volume = 1281, pages = "20--46" } @inproceedings{herman01:tlca, author={H. Geuvers}, title={Induction Is Not Derivable in Second Order Dependent Type Theory}, pages={166--181}, booktitle={Proceedings of {TLCA}'01}, year = {2001}, editor={S. Abramsky}, series=lncs, publisher=springer} @inproceedings{herman94:types, author={H. Geuvers}, title={A short and flexible proof of strong normalisation for the {C}alculus of {C}onstructions}, booktitle={Proceedings of {TYPES}'94}, editor={P. Dybjer and B. Nordstr{\"o}m and J. Smith}, year={1995}, series=lncs, pages={14-38}, crossref={types94}, publisher=springer} @inproceedings{herman93:bra, author={H. Geuvers}, title={Conservativity between logics and typed $\lambda$-calculi}, booktitle={Proceedings of {TYPES}'93}, year={1993}, series=lncs, pages={79--107}, crossref={types93}, publisher=springer} @inproceedings{GPZ99:csl, editor = {J. Flum and M. Rodr\'{\i}guez-Artalejo}, booktitle = {Proceedings of {CSL}'99}, publisher = springer, series = lncs, volume = {1683}, year = {1999}, author={H. Geuvers and E. Poll and J. Zwanenburg}, title={Safe Proof Checking in Type Theory with {Y}}, pages={439--452}} @inproceedings{GS05:vmcai, author={S. Genaim and F. Spoto}, title={{Information Flow Analysis for Java Bytecode}}, booktitle={Proceedings of {VMCAI}'05}, publisher = springer, series = lncs, volume = {3385}, year = {2005}, editor = {R. Cousot}, pages = {346--362}, } @InProceedings{GWZ00:tphol , Author={H. Geuvers and F. Wiedijk and J. Zwanenburg} , Title={Equational reasoning via partial reflection} ,Booktitle={Proceedings of {TPHOLs}'00} , Year= 2000 , Publisher= springer , series= lncs , volume= {1869} , Editor= {M. Aagard and J. Harrison} , pages={162--178}} @inproceedings{gha96:csl, author={N. Ghani}, title={Eta-expansions: {$F^{\omega}$}}, booktitle={Proceedings of {CSL}'96}, year={1997}, series=lncs, editor={D. van Dalen and M. Bezem}, publisher=springer, year={1997}, volume={1258}, pages={182--197}} @inproceedings{gha97:tlca, AUTHOR = {Ghani, N.} , TITLE = {Eta-expansions in Dependent Type Theory---the Calculus of Constructions} , YEAR = 1997 , volume={1210} , editor ={P. de Groote and J. Hindley} , booktitle={Proceedings of TLCA'97} , publisher =springer, pages={164--180}, series=lncs} @InProceedings{GM05:formats, title = "Timed Abstract Non-interference", author = "R. Giacobazzi and I. Mastroeni", booktitle = "Proceedings of {FORMATS}'05", publisher = springer, year = "2005", editor = "P. Pettersson and W. Yi", pages = "289--303", series = lncs, volume= "3829" } @Inproceedings{eduardo95:bra, author = "E. Gim{\'e}nez", title = "An Application of Co-Inductive Types in {Coq}: An Experiment with the Alternating Bit Protocol", editor = "S. Berardi and M. Coppo", booktitle = "Proceedings of {TYPES}'95", series = lncs, volume = "1158", pages = "135--152", publisher = springer, year = "1996" } @InProceedings{eduardo98:icalp , Author ={E. Gim{\'e}nez} , Title={Structural recursive definitions in {T}ype {T}heory} ,Booktitle={Proceedings of ICALP'98} , Year= 1998 , Publisher=springer , series= lncs , volume= {1443} , Editor= {K.G. Larsen and S. Skyum and G. Winskel} , pages={397--408}} @inproceedings{healf94:bra, author={H. Goguen}, title={The metatheory of UTT}, booktitle={Proceedings of {TYPES}'94}, editor={P. Dybjer and B. Nordstr{\"o}m and J. Smith}, year={1995}, series=lncs, pages={60-82}, crossref={types94}, publisher=springer} @incollection(obj3, title = "An Introduction to {OBJ3}", author = "J. Goguen and C. Kirchner and H. Kirchner and A. M\'egrelis and J. Meseguer", booktitle = "Proceedings of CTRS'88", editor = "J.-P. Jouannaud and S. Kaplan", publisher =springer, series=lncs, volume={308}, year = 1988, pages = "258--263") @InProceedings{GJM85:icalp, title = "Operational semantics for order-sorted algebra", author = "J. Goguen and J.-P. Jouannaud and J. Meseguer", booktitle = {Proceedings of the ICALP'85}, year = "1985", pages = "221--231", editor = "W. Brauer", publisher = springer, series = lncs, volume = "194", } @InProceedings{GHL97:fsttcs, author={A.D. Gordon and P.D. Hankin and S.B. Lassen}, title={Compilation and Equivalence of Imperative Objects}, booktitle={Proceedings of FSTTCS'97}, pages={74--87}, year={1997}, editor={S. Ramesh and G. Sivakumar}, series=lncs, volume={1346}, publisher=springer} @inproceedings{jean00:fmppta, author={J. Goubault-Larrecq}, title={A Method for Automatic Cryptographic Protocol Verification (Invited Paper)}, booktitle={Proceedings of FMPPTA'2000}, year={2000}, volume={xxxx}, Publisher= springer, series= lncs, note={To appear}} @InProceedings{GS97:cav, author = "S. Graf and H. Saidi", year = "1997", title = "Construction of Abstract State Graphs with {PVS}", booktitle = "Proceedings of CAV'97", pages = "72--83", series=lncs, publisher=springer, volume=1254, editor="O. Grumberg" } @inproceedings{GKW96:disco, author={S. Gray and N. Kajler and P.S. Wang}, title={Pluggability issues in the multi-protocol}, year={1996}, Publisher= springer, series= lncs, booktitle={Proceedings of DISCO'96}, editor={J. Calmet and C. Limongelli}, volume={1128}, pages={343--356}} @InProceedings{GM05:tphols, title = "Proving Equalities in a Commutative Ring Done Right in Coq", author = "B. Gr{\'e}goire and A. Mahboubi", year = "2005", booktitle = "Proceedings of TPHOLs'05", pages = "98--113", editor="J. Hurd and T. Melham", volume="3603", Publisher= springer, series= lncs, } @INPROCEEDINGS{gro93:tlca, AUTHOR = "Groote, P. de", TITLE = "The Conservation Theorem revisited", BOOKTITLE = "Proceedings of {TLCA}'93", YEAR = 1993, EDITOR = "Bezem, M. and Groote, J.F.", PAGES = "163--178", crossref={tlca}} @InProceedings{gro94:caap, author = {Groote, P. de}, title = {A {CPS}-Translation of the $\lambda\mu$-Calculus}, booktitle = {Proceedings of CAAP'94}, editor = {Tison, S.}, volume = 787, series = LNCS, year = 1994, publisher = springer, pages = {85--99} } @InProceedings{gro95:tlca, author = {Groote, P. de}, title = {A Simple Calculus of Exception Handling}, crossref = {tlca95}, booktitle={Proceedings of {TLCA}'95}, pages = {201--215}, year={1995}} @inproceedings{HS04:tphols, author={N.A. Hamid and Z. Shao}, title={{Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code}}, booktitle={Proceedings of {TPHOLs}'04}, series = lncs, volume = "3223", pages = "118-135", publisher = springer, year = "2004", editor={K. Slind and A. Bunker and G. Gopalakrishnan}} @inproceedings{HS00:csl, author = "P. Hancock and A. Setzer", title = "Interactive Programs in Dependent Type Theory", editor = "P. Clote and H. Schwichtenberg", booktitle = "Proceedings of {CSL}'00", series = lncs, volume = "1862", pages = "317--331", publisher = springer, year = "2000"} @inproceedings{HM89:mpc, author={J. Hannan and D. Miller}, title={Deriving Mixed Evaluation from Standard Evaluation for a Simple Functional Language}, editor={J. van de Snepscheut}, pages={239--255}, volume={375}, booktitle={Proceedings of MPC'89}, year={1989}, series=lncs, publisher=springer} @inproceedings{HT93:hol, author={J. Harrison and L. Th{\'e}ry}, title={Extending the {HOL} theorem prover with a computer algebra system to reason about the reals}, booktitle={Proceedings of HOL'93}, year={1993}, editor={J.J. Joyce and C.-J.H. Seger}, series=lncs, pages={174--184}, volume={780}, publisher=springer} @Inproceedings{HBL99:fssj, author = "P. H. Hartel and M. J. Butler and M. Levy", title = "{The Operational Semantics of a Java Secure Processor}", series = lncs, volume = "1523", year = "1999", editor={J. Alves-Foss}, booktitle={Formal {S}yntax and {S}emantics of {J}ava}, pages={313--352}, PUBLISHER = springer} @inproceedings{john95:plilp, author={J. Hatcliff}, title={Mechanically Verifying the Correctness of an Offline Partial Evaluator}, pages={279--298}, booktitle={Proceedings of PLILP'95}, editor={M. Hermenegildo and D. Swierstra}, series=lncs, volume={982}, year={1995}, publisher=springer} @InProceedings{HG96:pe, author = "J. Hatcliff and R. Gl{\"u}ck", title = "Reasoning about Hierarchies of Online Program Specialization Systems", crossref = "DGT96:pe", pages = "161-182", editor = "O. Danvy and R. Gl{\"u}ck and P. Thiemann", volume = "1110", year = 1996, series=lncs, publisher=springer} @inproceedings{HD01:concur, author = "J. Hatcliff and M. Dwyer", title = "Using the Bandera Tool Set to Model-Check Properties of Concurrent {Java} Software", series = lncs, volume = "2154", pages = "39--58", year = "2001", editor={K. G. Larsen and M. Nielsen}, booktitle={Proceedings of CONCUR'01}, publisher=springer} @InProceedings{hat+05:esop, author = "V.~P.~ Ranganath and T.~Amtoft and A.~ Banerjee and M.~B.~Dwyer and J.~Hatcliff", title = "A New Foundation for Control-Dependence and Slicing for Modern Program Structures", booktitle = "Proceedings of ESOP'05", editor = "M. Sagiv", year = "2005", pages = "77--93", volume = "3444", series=lncs, publisher=springer} @inproceedings{hav99:spin, author={K. Havelund}, editor={D. Dams and R. Gerth and S. Leue and M. Massink}, booktitle={Proceedings of SPIN'99}, title={{Java PathFinder---A Translator from Java to Promela}}, year=1999, series= lncs, volume= {1680}, pages={152}, Publisher=springer} @InProceedings{HR00:icalp, author = "M. Hennessy and J. Riely", title = "Information Flow vs. Resource Access in the Information Asynchronous Pi-Calculus", booktitle = "Proceedings of {ICALP}'00", year = "2000", editor = "U. Montanari and J. D. P. Rolim and E. Welzl", volume = "1853", series = lncs, publisher = "Springer", pages = "415--427", } @inproceedings{hen+03:emsoft, author={T.A. Henzinger and C.M. Kirsch and S. Matic}, title={Schedule-Carrying Code}, series=lncs, volume = "2855", pages = "241 -- 256", year = "2003", booktitle={Proceedings of EMSOFT'03}, editor={R. Alur and I. Lee}} @inproceedings{hof00:esop, author = "M. Hofmann", title = "{A Type System for Bounded Space and Functional In-Place Update--Extended Abstract}", series=lncs, volume = "1782", pages = "165--179", year = "2001", booktitle={Proceedings of ESOP'00}, editor={G. Smolka}} @InProceedings{martin95:tlca , Author={M. Hofmann} , Title={{A Simple Model for Quotient Types}} ,Booktitle={{Proceedings of {TLCA}'95}} , Year= 1995 , Publisher=springer , series= lncs , volume= {902} , Editor= {M. Dezani-Ciancaglini and G. Plotkin} , pages={216-234} } @inproceedings{martin93:types, author = "M. Hofmann", title = "{Elimination of Extensionality in {M}artin-{L}{\"o}f's Type Theory}", volume = "806", pages = "166--190", year = "1994", Booktitle={{Proceedings of {TYPES}'93}}, editor={H. Barendregt and T. Nipkow}, Publisher=springer , series= lncs } @InProceedings{HVY00:esop, author = "K. Honda and V. Vasconcelos and N. Yoshida", title = "Secure Information Flow as Typed Process Behaviour", booktitle = "Proceedings of {ESOP}'00", year = "2000", editor = "G. Smolka", volume = "1782", series = lncs, publisher = springer, pages = "180--199", } @InProceedings{tony95:tlca, author = {Hurkens, A.}, title = {{A Simplification of Girard's Paradox}}, crossref = {tlca95}, booktitle={Proceedings of {TLCA}'95}, pages = {266--278}, year={1995} } @inproceedings{jac94:cade, author = {Jackson, P.} ,title = {Exploring Abstract Algebra in Constructive Type Theory} ,booktitle = "CADE'94" ,editor = {A. Bundy} ,publisher = {Springer} ,series = lnai ,year = {1994} } @inproceedings{bart01:esop, author = {B. Jacobs}, title = {{A Formalisation of Java's Exception Mechanism}}, year = {2001} , Booktitle={Proceedings of ESOP'01} , Publisher=springer , series= lncs , volume= {2028} , Editor= {D. Sands} , pages={284--301}} @INPROCEEDINGS{JP01:fase, AUTHOR = "B. Jacobs and E. Poll", TITLE = "A Logic for the {J}ava {M}odeling {L}anguage {JML}", BOOKTITLE = "Fundamental Approaches to Software Engineering (FASE)", EDITOR = "H. Hussmann", PUBLISHER = springer, SERIES = lncs, VOLUME = "2029", PAGES = "284--299", YEAR = 2001} @inproceedings{JLM05:esop, author={R. Janvier and Y. Lakhnech and L. Mazar\'e}, title={Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries}, booktitle={Proceedings of {ESOP}'05}, series=lncs, volume=3444, publisher=springer, editor={S. Sagiv}, pages={172-185}, year=2005} @InProceedings{JPZ02:fossacs, author={S. Jha and J. Palsberg and T. Zhao}, title={Efficient Type Matching}, pages={187--204}, editor = {M. Nielsen and U. Engberg}, booktitle ={Proceedings of FOSSACS 2002}, publisher=springer, series = lncs, volume = {2303}, year = {2002}} @InProceedings{JLS96:types, author={A. Jones and Z. Luo and S. Soloviev}, title={Some algorithmic and proof-theoretical aspects of coercive subtyping}, booktitle={Proceedings of {TYPES}'96}, editor={E. Gim{\'e}nez and C. Paulin-Mohring}, series=lncs, publisher=springer, volume={1512}, year={1998}} @inproceedings{jon00:esop, author = "M. P. Jones", title = "Type Classes with Functional Dependencies", series = lncs, volume = "1782", pages = "230-244", year = "2000", booktitle={Proceedings of ESOP'00}, editor={G. Smolka}} @inproceedings{Jou93:tr, author={J.-P. Jouannaud}, title={Introduction to Rewriting}, booktitle={Term rewriting}, pages={1-15}, crossref={CJ93}, editor={H. Comon and J.-P. Jouannaud}, series= lncs, PUBLISHER=springer, year={1993}, volume={909}} @Inproceedings{kah87:stacs, author = "G. Kahn", title = "Natural Semantics", booktitle = "Proceedings of the Symposium on Theoretical Aspects of Computer Science", publisher = springer, year = "1987", series = lncs, volume = "247", pages = "22--39", editor={F.-J. Brandenburg and G. Vidal-Naquet and M. Wirsing}} @INPROCEEDINGS{KW96:compass, author={J. Kamperman and H. Walters}, title={Minimal Term Rewriting Systems}, BOOKTITLE={Recent Trends in Data Type Specification}, SERIES=lncs, volume={1130}, pages={274--290}, year={1996}, editor={M. Haveraaen and O. Owe and O.-J. Dahl}} @inproceedings{KML98:plilp, title={Explicit Substitutions for Objects and Functions}, author={D. Kesner and P.E. Mart{\'\i}nez L{\'o}pez}, booktitle={Proceedings of PLILP'98/ALP'98}, pages = "195-212", year = 1998, volume = 1490, series = lncs, publisher = springer} @inproceedings{Kir93:tr, author={H. Kirchner}, title={Some extensions of rewriting}, booktitle={Term rewriting}, pages={54-73}, crossref={CJ93}, editor={H. Comon and J.-P. Jouannaud}, series= lncs, PUBLISHER=springer, year={1993}, volume={909}} @InProceedings{LLT05:rta, author = "P. Lafourcade and D. Lugiez and R. Treinen", booktitle = "{P}roceedings of {RTA}'05", editor = "J. Giesl", pages = "308--322", publisher = "Springer", series = lncs, title = "Intruder Deduction for {AC}-like Equational Theories with Homomorphisms", volume = "3467", year = "2005" } @inproceedings{lan00:zb, author = "J.-L. Lanet", title = "Are Smart Cards the Ideal Domain for Applying Formal Methods?", series=lncs, volume = "1878", pages = "363--374", year = "2000", booktitle = "Proceedings of ZB'2000", editor={J.P.~Bowen and S.~Dunne and A.~Galloway and S.~King} } @InProceedings{LR98:cardis, author = "J.-L. Lanet and A. Requet", title = "{Formal Proof of Smart Card Applets Correctness}", booktitle = "Proceedings of CARDIS'98", year = "1998", editor={J.-J. Quisquater and B. Schneier}, volume={1820}, pages={85--97}, series=lncs, publisher=springer} @inproceedings{LT97:tacs, author = "J. Lawall and P. Thiemann", title = "Sound Specialization in the Presence of Computational Effects", booktitle = "Proceedings of TACS'97", pages = "165-190", year = 1997, volume = 1281, series = lncs, publisher = springer} @inproceedings{LJ98:mpc, author = "K. Leino and R. Joshi", title = "A semantic approach to secure information flow", series=lncs, volume = "1422", pages = "254--271", year = "1998", booktitle={Proceedings of MPC'98}, editor={J. Jeuring} } @inproceedings{lei01:dagstuhl, author = "K. R. M. Leino", title = "{Extended Static Checking: A Ten-Year Perspective}", series = lncs, volume = "2000", pages = "157--175", year = "2001", booktitle={Informatics--10 Years Back, 10 Years Ahead}, editor={R. Wilhelm}} @INPROCEEDINGS{ler01:cav, AUTHOR = {X. Leroy}, TITLE = {{Java} bytecode verification: an overview}, BOOKTITLE = {Proceedings of CAV'01}, YEAR = 2001, PUBLISHER = springer, SERIES = lncs, VOLUME = 2102, PAGES = {265--285}, editor={G. Berry and H. Comon and A. Finkel} } @INPROCEEDINGS{ler01:esmart, AUTHOR = {X. Leroy}, TITLE = {On-card Bytecode Verification for {Java} Card}, BOOKTITLE = {Proceedings of {e-SMART}'01}, PUBLISHER = springer, YEAR = 2001, series=lncs, volume= {2140}, pages={150--164}, editor= {I. Attali and T. Jensen}} @InProceedings{LMMS99:fm, author = "P. Lincoln and J. Mitchell and M. Mitchell and A. Scedrov", title = "Probabilistic Polynomial-Time Equivalence and Security Analysis", editor = "J. M. Wing and J. Woodcock and J. Davies", booktitle = "Proceedings of {FM}'99---Volume~{I}", year = "1999", volume = "1708", series = lncs, publisher = springer, pages = "776--793"} @InProceedings{log04:vmcai, author = {F. Logozzo}, title = {Automatic Inference of Class Invariants}, booktitle = {Proceedings of {VMCAI}'04}, year = {2004}, volume = 2937, series = lncs, publisher = {Springer-Verlag}, pages={211-222}, editor="G.~Levi and B.~Steffen"} @inproceedings{low96:tacas, author={G. Lowe}, title={{Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR}}, booktitle={Proceedings of {TACAS}'96}, pages={147-166}, year={1996}, editor = {T. Margaria and B. Steffen}, publisher = springer, series = lncs, volume = {1055}} @inproceedings{luo96:csl, author = "Z. Luo", title = "Coercive Subtyping in Type Theory", booktitle={Proceedings of {CSL}'96}, series=lncs, editor={D. van Dalen and M. Bezem}, publisher=springer, year={1997}, volume={1258}, pages={275--296}} @Proceedings{LS99:ctcs, title = {Dependent Coercions}, author= {Z. Luo and S. Soloviev}, year = {1999}, editor = {M. Hofmann}, volume = {29}, series = entcs, publisher = elsevier, booktilte={Proceedings of CTCS'99} } @inproceedings{LLS02:types, editor={H. Geuvers and F. Wiedijk}, booktitle={Proceedings of {TYPES}'02}, volume={2646}, series=lncs, publisher=springer, year={2003}, title={Weak Transitivity in Coercive Subtyping}, author={Y. Luo and Z. Luo and S. Soloviev}, pages={220--239}} @inproceedings{LY97:fme, author = "S.-W. Yu and Z. Luo", title = "Implementing a model checker for Lego", booktitle={Proceedings of FME'97}, editor = "J. Fitzgerald and C. B. Jones and P. Lucas", volume = "1313", series = lncs, publisher = springer, year = "1997", pages = "442--458" } @inproceedings{MB00:types, author = "N. Magaud and Y. Bertot", title = "Changing Data Structures in Type Theory: A Study of Natural Numbers", booktitle = "Proceedings of {TYPES}'00", volume = "2277", pages = "181--196", year = "2002", editor={P. Callaghan and Z. Luo and J. McKinna and R. Pollack} } @inproceedings{nicolas03:tphols, author = "N. Magaud", title = "Changing Data Representation Within the Coq System", booktitle = "Proceedings of {TPHOLs}'03", volume = "2758", year = "2003", pages={87-102}, editor={D. Basin and B. Wolff} } @inproceedings{mai98:types, author={M.-E. Maietti}, title={{About Effective Quotients in Constructive Type Theory}}, pages={164--178}, booktitle={{Proceedings of {TYPES}'98}}, editor={T. Altenkirch and W. Naraschewski and B. Reus}, Publisher=springer, series= lncs, year={1999}, volume= {1657}} @inproceedings{MS04:aplas, author={H. Mantel and D. Sands}, title={{Controlled Declassification based on Intransitive Noninterference}}, booktitle={{Proceedings of APLAS'04}}, year=2004, Publisher=springer, series= lncs} @InProceedings{MSK06:lopstr, author = {H. Mantel and H. Sudbrock and T. Krausser}, title = {Combining Different Proof Techniques for Verifying Information Flow Security}, booktitle = {Pre-Proceedings of LOPSTR'06}, year = 2006, editor = {G. Puebla}, volume = {Raporta di Ricerca CS-2006-5, Universit{\`a} Ca'~Foscari Di Venezia} } @inproceedings{mat93:rta, Author = "B. Matthews", Title = "{MERILL}: An Equational Reasoning System in Standard {ML}", Booktitle = "Proceedings of RTA'93", Editor = "C. Kirchner", Series = lncs, Volume = 690, Pages = {441-445}, Publisher = springer, Year = 1993} @inproceedings{jamesrandy93:tlca, author={McKinna, J. and Pollack, R.}, title={Pure Type Systems Formalised}, pages={289--305}, series=lncs, publisher=springer, volume={664}, year={1993}, booktitle={Proceedings of {TLCA}'93}, crossref={tlca}} @InProceedings{mea01:mmm, author = "C. Meadows", title = "Open Issues in Formal Methods for Cryptographic Protocol Analysis", booktitle = "Proceedings of {MMMACNS}", year = "2001", series=lncs, publisher=springer, volume={2052}, editor = {V.I. Gorodetski and V.A. Skormin and L.J. Popyack}} @inproceedings{MCB05:ictcs, author="R. Medel and A. Compagnoni and E. Bonelli", title="A Typed Assembly Language for Non-Interference", booktitle="Proceedings of ICTCS 2005", pages={360-374}, series=lncs, publisher=springer, volume={3701}, year={2005}, editor="M. Coppo and E. Lodi and G.M. Pinna"} @inproceedings{MP01:esmart, author = {Meijer, H. and Poll, E.}, title = {Towards a full formal specification of the Java Card}, editor = {I. Attali and T. Jensen}, booktitle = {Proceedings of {e-SMART}'01}, series = lncs, publisher = springer, year = {2001}, volume = {2140}, pages = {165--178}, } @inproceedings{MW96:types, author={P.-A. Melli{\`e}s and B. Werner}, title={A generic proof of strong normalisation for pure type systems}, year={1998}, booktitle={Proceedings of {TYPES}'96}, editor={E. Gim{\'e}nez and C. Paulin-Mohring}, series=lncs, publisher=springer, volume={1512}} @inproceedings{MP00:tacas, author={J. Meyer and A. Poetzsch-Heffter}, title={An Architecture for Interactive Program Provers}, pages={63--77}, year={2000}, booktitle={Proceedings of TACAS'2000}, editor={S. Graf and M. Schwartzbach}, volume={1785}, series=lncs, publisher=springer} @INPROCEEDINGS{MW85:lp , AUTHOR = {Meyer, A.R. and M. Wand} , BOOKTITLE = {Logics of Programs} , SERIES = lncs , VOLUME = {193} , EDITOR = {Parikh, R.} , PUBLISHER = springer , PAGES = {219--224} , TITLE = {Continuation Semantics in typed lambda-calculi (summary)} , YEAR = 1985 } @inproceedings{miq01:tlca, author={A. Miquel}, title={The Implicit Calculus of Constructions}, booktitle={Proceedings of {TLCA}'01}, pages={344--359}, volume = {2044}, year = {2001}, editor={S. Abramsky}, series=lncs, publisher=springer} @inproceedings{MW02:types, editor={H. Geuvers and F. Wiedijk}, booktitle={Proceedings of {TYPES}'02}, volume={2646}, series=lncs, publisher=springer, year={2003}, title={The Not So Simple Proof-Irrelevant Model of CC}, author={A. Miquel and B. Werner}, pages={240--258}} @inproceedings{mit95:fct, author={J. Mitchell and K. Fischer}, title={A delegation-based object calculus with subtyping}, booktitle={Proceedings of FCT'95}, series=lncs, volume={965}, year={1995}, pages={42-61}, Publisher= springer, editor={H. Reichel}} @inproceedings{Moh89:rta, author={C. Mohan}, title={Priority rewriting: semantics, confluence and conditionals}, booktitle={Proceedings of RTA'89}, year={1989}, editor={N. Dershowitz}, pages={278-291}, volume={355}, series=lncs, publisher=springer} @inproceedings{MS89:rta, author={C. Mohan and M. Srivas}, title={Negation with logical variables in conditional rewiting}, booktitle={Proceedings of RTA'89}, year={1989}, editor={N. Dershowitz}, pages={292-310}, volume={355}, series=lncs, publisher=springer} @inproceedings{nau05:tphols, author={D. Naumann}, title={Verifying a Secure Information Flow Analyzer}, year={2005}, booktitle="Proceedings of TPHOLs'05", series=lncs, publisher=springer, pages="211-226", volume={3603}, editor={J.~Hurd and T.~Melham}, note={Preliminary version appears as Report CS-2004-10, Stevens Institute of Technology, 2003}} @inproceedings{nau06:esorics, author={D. Naumann}, title={From coupling relations to mated invariants for checking information flow (extended abstract)}, year={2006}, booktitle="Proceedings of ESORICS'06", series=lncs, publisher=springer, pages="xxx-xxx", volume={3xxx}, editor={D.~Gollmann and A.~Sabelfeld}, note={To appear}} @InProceedings{NN96:pe, author = "F. Nielson and H.R. Nielson", title = "Multi-Level Lambda-Calculi: an Algebraic Description", booktitle = "Partial Evaluation", editor = "O. Danvy and R. Gl{\"u}ck and P. Thiemann", volume = "1110", pages = "338-354", year = 1996, series=lncs, publisher=springer, crossref ="DGT96:pe"} @InProceedings{NN98:mfcs , Author ={F. Nielson and H.R. Nielson} , Title={{Flow analyis for imperative objects}} ,Booktitle={Proceedings of MFCS'98} , Year= 1998 , Publisher=springer , series= lncs , volume= {1450} , Editor= {L. Brim and J. Gruska and J. Zlatuska} , pages={220--228}} @inproceedings{nip01:fossacs, author = {T. Nipkow}, title = {{Verified Bytecode Verifiers}}, year = {2001} , Booktitle={Proceedings of FOSSACS'01} , Publisher=springer , series= lncs , volume= {2030} , Editor= {F. Honsell and M. Miculan} , pages={347--363} } @book{isabelle, title={{Isabelle/HOL: A Proof Assistant for Higher-Order Logic}}, author={T. Nipkow and L. C. Paulson and M. Wenzel}, series=lncs, publisher=springer, year={2002}, volume={2283}} @inproceedings{NB03:types, author={M. Niqui and Y. Bertot}, title={{QArith: Coq Formalisation of Lazy Rational Arithmetic}}, editor={S. Berardi and M. Coppo and F. Damiani}, booktitle={{Proceedings of TYPES'03}}, volume=3085, publisher=springer, pages={309--323}, year={2004}} @InCollection{vO99:fsttcs, author = "D. von Oheimb", title = "Hoare logic for mutual recursion and local variables", booktitle = "Proceedings of FSTTCS'99", pages = "168--180", year = "1999", volume = "1738", series = lncs, editor = "C. {Pandu, Rangan} and V. Raman and R. Ramanujam", publisher = springer} @InProceedings{par92:lpar, author = {Parigot, M.}, title = {$\lambda\mu$-Calculus: An Algorithmic Interpretation of Classical Natural Deduction}, booktitle = {Proceedings of {LPAR}'92}, volume = 624, series = lncs, year = 1992, publisher = springer, pages = {190--201} } @INPROCEEDINGS{pau93:tlca , AUTHOR = {C. Paulin-Mohring} , TITLE = {Inductive Definitions in the System {C}oq. {R}ules and Properties} , BOOKTITLE = tlca1 , EDITOR = {M. Bezem and J.F. Groote} , SERIES = lncs , VOLUME = 664 , PUBLISHER = springer , YEAR = 1993 , CROSSREF = {tlca} , PAGES = {328--345} } @book{isabelle94, title={Isabelle: a generic theorem prover}, author={L. Paulson}, series= lncs, volume={828}, PUBLISHER=springer, year={1994}} @inproceedings{elf, AUTHOR="F. Pfenning", TITLE="Elf: a meta-language for deductive systems", BOOKTITLE="Proceedings of CADE-12", EDITOR="A. Bundy", PAGES="811--815", series=lnai, volume={814}, PUBLISHER="Springer-Verlag", YEAR={1994}} @InProceedings{PP89:mfps, author = "F. Pfenning and C. Paulin", title = "{Inductively Defined Types in the Calculus of Constructions}", booktitle = "Proceedings of MFPS'89", editor = "M. Main and A. Melton and M. Mislove and D. Schmidt", year = 1989, series =lncs, pages={209-228}, publisher=springer, volume=442} @InProceedings{PW95:mfps, author = "F. Pfenning and H.-C. Wong", title = "On a Modal $\lambda$-Calculus for {S4}", booktitle = "Proceedings of the Eleventh Conference on Mathematical Foundations of Programming Semantics", editor = "S. Brookes and M. Main", year = 1995, series =entcs, volume=1} @INPROCEEDINGS{pit87:ctcs, AUTHOR = "A. Pitts", TITLE = "Polymorphism is set theoretic, constructively", BOOKTITLE = "Category and Computer Science", EDITOR = "D.H. Pitt and A. Poign\'{e} and D.E. Rydeheard", PAGES = "12--39", PUBLISHER = springer, SERIES = lncs, VOLUME = "283", YEAR = 1987} @InProceedings{plu90:ctrs, author={D. Plump}, title={Implementing term rewriting by graph reduction: termination of combined systems}, series=lncs, booktitle={Proceedings of CTRS'90}, year={1991}, pages={307--317}, editor={S. Kaplan and M. Okada}, volume={516}} @inproceedings{PSS98:tacas, title = "Translation Validation", author = "A. Pnueli and E. Singerman and M. Siegel", year = "1998", Booktitle={Proceedings of {TACAS}'98} , Publisher=springer , series= lncs , volume= {1384} , Editor= {B. Steffen} , pages={151--166} } @InProceedings{PM99:esop, author={A. Poetzsch-Heffter and P. Mller}, title={{A Programming Logic for Sequential Java}}, year={1999}, Booktitle={Proceedings of ESOP'99} , Publisher=springer , series= lncs , volume= {1576} , Editor= {D. Swiestra} , pages={162-176}} @inproceedings{erik98:kyoto, author = {E. Poll}, booktitle = {Proceedings of Theories of Types and Proofs (TTP) - Kyoto}, organization = {Kyoto University Research Insitute for Mathematical Sciences}, pages = {112-125}, series = {RIMS Lecture Notes 1023}, title = {{S}ubtyping and {I}nheritance for {C}ategorical {D}atatypes}, year = {1998} } @InProceedings{randy94:types, author ="R. Pollack", title ={On Extensibility of Proof Checkers}, pages={140-161}, booktitle ={Proceedings of {TYPES}'94}, editor ={P.Dybjer and B.Nordstr\"om and J.Smith}, series =lncs, volume={996}, year ={1995}, crossref={types94}, publisher ="Springer-Verlag"} @InProceedings{randy95:tlca , Author={R. Pollack} , Title={A verified type-checker} ,Booktitle={Proceedings of {TLCA}'95} , Year= 1995 , Publisher= springer , series= lncs , volume= {902} , Editor= {M. Dezani-Ciancaglini and G. Plotkin} , pages={365--380} , month={April} , crossref={tlca95}} @InProceedings{randy00:tphols , Author={R. Pollack} , Title={Dependently typed records for representing mathematical structures} ,Booktitle={Proceedings of {TPHOLs}'00} , Year= 2000 , Publisher= springer , series= lncs , volume= {1869} , Editor= {M. Aagard and J. Harrison} , pages={462--479}} @inproceedings{olivier00:types, author = "O. Pons", title = "Generalization in Type Theory Based Proof Assistants", booktitle = "Proceedings of {TYPES}'00", volume = "2277", pages = "217--232", year = "2002", editor={P. Callaghan and Z. Luo and J. McKinna and R. Pollack} } @InProceedings{PV98:esorics, author = "J. Posegga and H. Vogt", title = "{Byte Code Verification for Java Smart Cards Based on Model Checking}", booktitle = "Proceedings of {ESORICS}'98", publisher = springer, volume = "1485", year = "1998", editor = "J.-J. Quisquater and Y. Deswarte and C. Meadows and D. Gollmann", series = lncs, pages = "175--190", } @inproceedings{pus99:tacas, author = {C. Pusch}, title = {Proving the Soundness of a {J}ava Bytecode Verifier Specification in {Isabelle/HOL}}, booktitle = {Proceedings of TACAS'99}, series =lncs, volume = {1579}, year = {1999}, publisher = springer, editor = {W. R. Cleaveland}, pages = {89--103}} @InProceedings{qia90:alp, author = "Z. Qian", title = "Higher-order order-sorted algebras", booktitle = {Proceedings of ALP'90}, publisher = springer, SERIES = lncs, year = "1990"} @Inproceedings{qia99:fssj, author = "Z. Qian", title = "{A Formal Specification of Java Virtual Machine Instructions for Objects, Methods and Subroutines}", series=lncs, volume = "1523", year = "1999", editor={J. Alves-Foss}, pages={271--312}, booktitle={Formal {S}yntax and {S}emantics of {J}ava}, publisher=springer } @inproceedings{qia99:types, editor = {T. Coquand and P. Dybjer and B. Nordstr{\"o}m and J. Smith}, booktitle = {{Proceedings of {TYPES}'99}}, publisher = springer, series = lncs, volume = {1956}, year = {2000}, author={H. Qiao}, title={{Formalising Formulas-as-Types-as-Objects}}, pages={174--193}} @inproceedings{qui03:tphols, author={C.L. Quigley}, title={{A Programming Logic for Java Bytecode Programs}}, booktitle={Proceedings of {TPHOLs}'03}, pages={41--54}, volume = "2758", year = "2003", series=lncs, publisher=springer, editor={D. Basin and B. Wolff} } @INPROCEEDINGS{RS94:tacs , AUTHOR = {Rehof, N.J. and M.H. S{\o}rensen} , TITLE = {The $\lambda_{\Delta}$ calculus} , BOOKTITLE = {Proceedings of TACS'94} , SERIES = lncs , VOLUME = 789 , EDITOR = {Hagiya, M. and J. Mitchell} , PUBLISHER = springer , PAGES = {516--542} , YEAR = 1994 } @inproceedings{didier:appsem, author={D. R{\'e}my}, title={{Using, Understanding, and Unraveling the OCaml Language---From Practice to Theory and vice versa}}, booktitle={Proceedings of APPSEM'2000}, editor={G. Barthe and P. Dybjer and L. Pinto and J. Saraiva}, volume={2395}, series=lncs, publisher=springer, year={2002}} @InProceedings{rey74:ps, author = {Reynolds, J.}, title = {Towards a Theory of Type Structure}, booktitle = {Proceedings of the Programming Symposium}, editor = {Robinet, B.}, volume = 19, series = lncs, year = 1974, publisher = springer, pages = {408--425} } @Inproceedings{rey84:sdt, AUTHOR = "J.C. Reynolds", TITLE = "Polymorphism is not set-theoretic", BOOKTITLE = "Semantics of Data Types", SERIES = lncs, VOLUME = 173, EDITOR = "G. Kahn and D.B. MacQueen and G.D. Plotkin", PUBLISHER = springer, PAGES = "145--156", YEAR = 1984} @InProceedings{PRW96:cade, author = {E. Ritter and D. Pym and L. Wallen}, title = {Proof-terms for Classical and Intuitionistic Logic (extended abstract)}, booktitle = {Proceeedings of CADE'96}, series=lnai, volume={1104}, year={1996}, pages={17--31}, editor={M. McRobbie and J. Slaney}} @InProceedings{PRW96:tableau, author = {E.~Ritter and D.~Pym and L.~A.~Wallen}, title = {On the Intuitionistic Force of Classical Search}, booktitle = {Proceedings of TABLEAU'96}, editor = {P.~Miglioli and U.~Moscato and D.~Mundici and M.~Ornaghi}, volume = 1071, series = lnai, year = 1996, publisher = springer, pages = {295--311}} @INPROCEEDINGS{PR95:tlca, AUTHOR={E.~Ritter and A.M.~Pitts}, TITLE={A Fully Abstract Translation between a $\lambda$-Calculus with Reference Types and {Standard} {M}{L}}, BOOKTITLE=tlca2, SERIES={Lecture Notes in Computer Science}, VOLUME={902}, PUBLISHER=springer, YEAR=1995, PAGES={397--413}, EDITOR = {M. Dezani-Ciancaglini and G. Plotkin}} @INPROCEEDINGS{riv03:vmcai, author={X. Rival}, title={{Abstract Interpretation-Based Certification of Assembly Code}}, booktitle={Proceedings of {VMCAI}'03}, pages={41--55}, series=lncs, volume={2575}, year={2003}, editor={L.D. Zuck and P.C. Attie and A.Cortesi and S. Mukhopadhyay}} @inproceedings{robby+04:tacas, title={Checking Strong Specifications Using An Extensible Software Model-checking Framework}, author={Robby and E. Rodr\'iguez and M.B. Dwyer and J. Hatcliff}, booktitle="Proceedings of TACAS'04", series=lncs, volume={2988}, year={2004}, editor={K. Jensen and A. Podelski}, pages={404-420}} @inproceedings{rod+05:ecoop, title="Extending JML for Modular Specification and Verification of Multi-Threaded Programs", author="E.~Rodriguez and M.B. Dwyer and C.~Flanagan and J.~Hatcliff and G.T.~Leavens and Robby", booktitle="Proceedings of ECOOP'05", series=lncs, VOLUME={3xxx}, PUBLISHER=springer, year={2005}} @Inproceedings{rus99:fm, author = "Rushby, J.", title = "Mechanized Formal Methods: Where Next?", booktitle = "Proceedings of FM'99 (volume 1)", series=lncs, VOLUME={1708}, PUBLISHER=springer, year={1999}, PAGES={48--51}, EDITOR= {J. Wing and J. Woodcock}} @InProceedings{RS99:tacas, title = "On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction", author = "V. Rusu and E. Singerman", booktitle = "Proceedings of TACAS'99", editor = "W. R. Cleaveland", pages = "178--192", publisher = springer, series = lncs, volume = "1579", year={1999} } @InProceedings{SS99:esop, author={A. Sabelfeld and D. Sands}, title={{A PER model of secure information flow in sequential programs}}, year={1999}, Booktitle={Proceedings of ESOP'99} , Publisher=springer , series= lncs , volume= {1576} , Editor= {D. Swiestra} , pages={40--58}} @INPROCEEDINGS{sab01:psi, author = {A.~Sabelfeld}, title = {The Impact of Synchronisation on Secure Information Flow in Concurrent Programs}, booktitle = {Proceedings of PSI'01}, pages = {227--241}, year = {2001}, series = lncs, volume = {2244}, publisher = springer } @inproceedings{SM03:isss, author={A.~Sabelfeld and A.~Myers}, title={A model for delimited information release}, booktitle = {Proceedings of {ISSS}'03}, year = {2004}, series = lncs, publisher = springer, pages={174--191}, editor={K.~Futatsugi and F.~Mizoguchi and N.~Yonezaki}, volume={3233}} @InProceedings{SS98:sas, author = "D. Schmidt and B. Steffen", title = "Program Analysis as Model Checking of Abstract Interpretations", booktitle = "Proceedings of SAS'98", series = "Lecture Notes in Computer Science", publisher = "Springer", editor = "G. Levi", volume = "1503", pages = "351--381", year = "1998"} @inproceedings{SMH01:lncs, author = "F. B. Schneider and G. Morrisett and R. Harper", title = "{A Language-Based Approach to Security}", series=lncs, volume = "2000", pages = "86--101", year = "2001", booktitle={{Informatics: 10 Years Back, 10 Years Ahead}}, editor={R. Wilhelm}} @inproceedings{sch01:icics, author={C.-P. Schnorr}, title={{Security of Blind Discrete Log Signatures against Interactive Attacks}}, booktitle={Proceedings of {ICICS}'01}, pages={1-12}, editor = {S. Qing and T. Okamoto and J. Zhou}, publisher = springer, series = lncs, volume = {2229}, year = {2001}} @inproceedings{SJ00:asiacrypt, author={C.-P. Schnorr and M. Jakobsson}, title={{Security of Signed ElGamal Encryption}}, booktitle={Proceedings of ASIACRYPT'00}, pages={73-89}, year={2000}, series=lncs, publisher=springer, volume={1976}, editor={T. Okamoto}} @InProceedings{schr97:tapsoft, author = "T. Schreiber", title = "Auxiliary Variables and Recursive Procedures", editor = "M. Bidoit and M. Dauchet", booktitle = "Proceedings of {TAPSOFT}'97", series = lncs, publisher = springer, volume = "1214", year = "1997", pages = "697--711" } @InProceedings{SLCM99:ecoop, title = {{Toward Automatic Specialization of Java Programs}}, author={U.P. Schultz and J. Lawall and C. Consel and G. Muller}, year = {1999}, editor = {R. Guerraoui}, volume = {1628}, series = lncs, publisher = springer, pages= {367--390}, booktitle={Proceedings of ECOOP'99}} @InProceedings{SYY03:aplas, title = "{Automatic Construction of Hoare Proofs from Abstract Interpretation Results}", author = "S. Seo and H. Yang and K. Yi", year = "2003", booktitle = "Proceedings of APLAS'03", pages = "230--245", volume = {2895}, series = lncs, publisher = springer, editor="A. Ohori" } @InProceedings{SP94:lfcs, author = "P. Severi and E. Poll", title = "Pure Type Systems with Definitions", booktitle = "Proceedings of LFCS'94", year = {1994}, editor= {A. Nerode and Y.N. Matiyasevich}, volume = {813}, series = lncs, pages = "316--328", publisher = springer, crossrefonly={lfcs94}} @inproceedings{sho97:eurocrypt, author = "V. Shoup", title = "Lower Bounds for Discrete Logarithms and Related Problems", series = lncs, booktitle={Proceedings of {EUROCRYPT}'97}, volume = "1233", pages = "256-266", year = "1997", editor={W. Fumy}, publisher=springer} @inproceedings{SW00:esop, author={S. F. Smith and T. Wang}, title={{Polyvariant flow analysis with constrained types}}, booktitle={Proceedings of ESOP'00}, pages={382--396}, editor={G. Smolka}, series= lncs, PUBLISHER=springer, year={2000}, volume={1782}} @INCOLLECTION{spr93:tlca , AUTHOR = {Springintveld, J.} , TITLE = {Lower and upper bounds for reductions of types in $\lambda \underline{\omega}$ and $\lambda {P}$} , BOOKTITLE = tlca1 , EDITOR = {M. Bezem and J.F. Groote} , SERIES = lncs , VOLUME = 664 , PUBLISHER = springer , YEAR = 1993 , CROSSREF = {tlca} , PAGES = {391--405} } @inproceedings{mh95:types, author={M. Stefanova and H. Geuvers}, title={A simple set-theoretic semantics for the {C}alculus of {C}onstructions}, booktitle={Proceedings of {TYPES}'95}, EDITOR ={S. Berardi and M. Coppo} , SERIES = lncs , PUBLISHER = springer , volume={1158} , YEAR = 1996 , crossref={types95} ,pages={249--264}} @inproceedings{ste03:eurocrypt, author={J. Stern}, title={Why Provable Security Matters?}, booktitle={Proceedings of {EUROCRYPT}'03}, pages={449-461}, editor = {E. Biham}, publisher = springer, series = lncs, volume = {2656}, year = {2003}} @inproceedings{str02:cade, author={M. Strecker}, title={{Formal Verification of a Java Compiler in Isabelle}}, booktitle={Proceedings of CADE'02}, EDITOR ={A. Voronkov} , SERIES = lncs , PUBLISHER = springer , volume={2392} ,year={2002} ,pages={63--77}} @InProceedings{str02:lpar, author = {M. Strecker}, title = {Investigating Type-Certifying Compilation with {Isabelle}}, booktitle = {Proceedings of {LPAR}'02}, year = 2002, volume = 2514, series = lncs, publisher = springer, editor={M. Baaz and A. Voronkov}, pages={403-417} } @InProceedings{SBN04:sas, title = "Modular and Constraint-Based Information Flow Inference for an Object-Oriented Language", author = "Q. Sun and A. Banerjee and D.A. Naumann", year = "2004", booktitle = "Proceedings of SAS'04", pages = "84--99", series=lncs, publisher=springer, volume=3148, editor="R. Giacobazzi" } @Inproceedings{sym99:fssj, author = "D. Syme", title = "Proving {Java} Type Soundness", series = lncs, volume = "1523", year = "1999", editor={J. Alves-Foss}, pages={83--118}, booktitle={Formal {S}yntax and {S}emantics of {J}ava}, PUBLISHER = springer} @inproceedings{SG02:lpar, author = "D. Syme and A. D. Gordon", title = "Automating Type Soundness Proofs via Decision Procedures and Guided Reductions", series = lncs, volume = "2514", pages = "418--434", year = "2002", booktitle={Proceedings of {LPAR}'02}, editor={M. Baaz and A. Voronkov}} @INPROCEEDINGS{TAH94:tacs , AUTHOR = {M. Takahashi and Y. Akama and S. Hirokawa} , TITLE = {Normal proofs and their grammar} , BOOKTITLE = {Proceedings of TACS'94} , SERIES = lncs , VOLUME = 789 , EDITOR = {Hagiya, M. and J. Mitchell} , PUBLISHER = springer , PAGES = {465-494} , YEAR = 1994 } @InProceedings{TA05:sas, title = "Secure Information Flow as a Safety Problem", author = "T. Terauchi and A. Aiken", booktitle = "Proceedings of {SAS}'05", publisher = springer, year = "2005", volume = "3672", editor = "C.~Hankin and I.~Siveroni", pages = "352--367", series = lncs } @InProceedings{ter95:amast, author = "D. Terrasse", title = "Encoding Natural Semantics in {Coq}", booktitle = "Proceedings of AMAST'95", editor = "V. S. Alagar", publisher = springer, series=lncs, volume=" 936", year = "1995", pages = "230--244" } @InProceedings{laurent98:cade, author = "L. Th{\'e}ry", title = "A Certified Version of {Buchberger's} Algorithm", pages = "349--364", editor = "C. Kirchner and H. Kirchner", booktitle = "Proceedings of {CADE}'98", series = lnai, volume = "1421", publisher = springer, year = "1998" } @InProceedings{thi97:tapsoft, author = "P. Thiemann", title = "A Unified Framework for Binding-Time Analysis", booktitle = "TAPSOFT'97", editor = "M. Bidoit and M. Dauchet", year = "1997", pages = "742--756", series = lncs, publisher = springer, VOLUME ="1214"} @InProceedings{TKB:rta89, author = "Y. Toyama and J.W. Klop and H. Barendregt", year = "1989", title = "Termination for the Direct Sum of Left-Linear Term Rewriting Systems", booktitle = "Proceedings of RTA'89", editor = "N. Dershowitz", series = lncs, pages = "477--491", publisher = springer, volume={355}} @inproceedings{TH02:amast, title = {{Extending JML Specifications with Temporal Logic}}, author = "K. Trentelman and M. Huisman", year = 2002, booktitle ="Proceedings of AMAST'02", publisher = springer, series = lncs, pages = "334-348", volume = 2422, editor = "H. Kirchner and C. Ringeissen" } @InProceedings{VHU92:cc, author = "J. Vitek and R. N. Horspool and J. Uhl", title = "Compile-time analysis of object-oriented programs", booktitle = "Proceedings of CC'92", publisher = springer, year = "1992", volume = "641", pages = "236--??"} @InProceedings{VS97:tapsoft, author = "D. Volpano and G. Smith", title = "{A Type-Based Approach to Program Security}", editor = "M. Bidoit and M. Dauchet", booktitle = "Proceedings of {TAPSOFT}'97", series = lncs, publisher = springer, volume = "1214", year = "1997", pages = "607--621"} @inproceedings{VS98:mas, author = "D. Volpano and G. Smith", title = "{Language Issues in Mobile Program Security}", pages = "25--43", booktitle = "Mobile Agent Security", editor = "G. Vigna", year = "1998", series = lncs, volume="1419", publisher =springer} @inproceedings{benjamin97:tacs, author = "B. Werner", title = "{Sets in Types, Types in Sets}", volume = "1281", booktitle = "{Proceedings of TACS'97}", pages = "530--546", year = "1997", editor={M. Abadi and T. Ito}, publisher =springer, series=lncs} @inproceedings{WN05:esop, title={Asserting Bytecode Safety}, author={M. Wildmoser and T. Nipkow}, booktitle={Proceedings of {ESOP}'05}, volume={3444}, editor ={S. Sagiv}, publisher =springer, series=lncs, year={2005}, pages={326-341}} @inproceedings{xi97:tlca, AUTHOR = {Xi, H.} , TITLE = {Weak and Strong Normalisations in typed $\lambda$-calculi} , YEAR = 1997 , volume={1210} , editor ={P. de Groote and J. Hindley} , booktitle=tlca3 , publisher =springer, series=lncs} @inproceedings{xi97:lfcs, author={H. Xi}, title={Simulating $\eta$-expansions with $\beta$-reductions in the Second-Order Polymorphic lambda-calculus}, year={1997}, booktitle={Proceedings of LFCS'97}, series=lncs, publisher =springer, editor={S. Adian and A. Nerode}, volume={1234}, pages={399--409}} @inproceedings{xi99:padl, author = "Xi, H.", title = {{Dead Code Elimination through Dependent Types}}, booktitle = "Proceedings of PADL'99", year = 1999, publisher =springer, volume={1551}, pages = "228--242", editor={G. Gupta}} @InProceedings{sha+03:esop, author = {D. Yu and N. A. Hamid and Z. Shao}, title = {Building Certified Libraries for {PCC}: Dynamic Storage Allocation}, booktitle = {Proceddings of {ESOP}'03}, year = 2003, editor={P. Degano}, pages={363--379}, volume={2618}, publisher= springer, series= lncs, } @InProceedings{sha+03:cc, author = {C. League and Z. Shao and V. Trifonov}, title = {{Precision in Practice: A Type-Preserving Java Compiler}}, pages={106--120}, booktitle = {Proceddings of {CC}'03}, year = 2003, editor={G. Hedin}, volume={2622}, publisher= springer, series= lncs, } @InProceedings{YI06:esop, title = "A Typed Assembly Language for Confidentiality", author = "D. Yu and N. Islam", year = "2006", booktitle = "Proceedings of ESOP'06", pages = "162--179", editor="P. Sestoft", volume=3924, publisher= springer, series= lncs} @INPROCEEDINGS{ZM01:esop, AUTHOR = {S. Zdancewic and A. Myers}, TITLE = {Secure Information Flow and {CPS}}, BOOKTITLE = {Proceedings of {ESOP}'01}, PUBLISHER = springer, SERIES = lncs, YEAR = {2001}, editor={D. Sands}, volume={2028}, pages={46--61}} @inproceedings{zha92:ctrs, author={H. Zhang}, title={Proving group isomorphisms theorems}, booktitle={Proceedings of CTRS'92}, year={1992}, Publisher= springer, series= lncs, editor={M. Rusinovitch and J.-L. Remy}, pages={302-306}} @inproceedings{zwa99:tlca, author={J. Zwanenburg}, title={Pure Type Systems with Subtyping}, booktitle={Proceedings of {TLCA}'99}, year=1999, Publisher=springer, series= lncs, editor={J.-Y. Girard}, pages={381--396}, volume=1581} %%%%%%%%%%%%% STOPPED HERE %%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @INPROCEEDINGS{fri78 , AUTHOR = {Friedman, H.} , TITLE = {Classically and Intuitionistically Provably Recursive Functions} , BOOKTITLE = {Higher Set-theory} , SERIES = lncs , VOLUME = 669 , EDITOR = {M\"uller, G.H. and Scott, D.S} , PUBLISHER = springer , PAGES = {21--28} , YEAR = 1978} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%% PROCEEDINGS %%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @PROCEEDINGS{tlca , TITLE = tlca1 , EDITOR = {M. Bezem and J.F. Groote} , SERIES = lncs , VOLUME = 664 , PUBLISHER = springer , YEAR = 1993 } @PROCEEDINGS{tlca95 , TITLE = tlca2 , EDITOR = {M. Dezani-Ciancaglini and G. Plotkin} , SERIES = lncs , VOLUME = 902 , PUBLISHER = springer , YEAR = 1995 } @PROCEEDINGS{tlca97 , TITLE = tlca3 , EDITOR = {P. de Groote and R. Hindley} , SERIES = lncs , VOLUME = 1210 , PUBLISHER = springer , YEAR = 1997 } @PROCEEDINGS{types93 , TITLE ={Proceedings of {TYPES}'93} , EDITOR ={H. Barendregt and T. Nipkow} , SERIES = lncs , VOLUME = 806 , PUBLISHER = springer , YEAR = 1994 } @PROCEEDINGS{types94 , TITLE ={Proceedings of {TYPES}'94} , EDITOR ={P. Dybjer and B. Nordstr{\"o}m and J. Smith} , SERIES = lncs , VOLUME = 996 , PUBLISHER = springer , YEAR = 1995 } @PROCEEDINGS{types95 , TITLE ={Proceedings of {TYPES}'95} , EDITOR ={S. Berardi and M. Coppo} , SERIES = lncs , PUBLISHER = springer , YEAR = 1996 , volume={1158}} @proceedings{cade94, title={Proceedings of CADE-12}, editor={A. Bundy}, volume=814, series=lnai, year={1994}, publisher=springer} @proceedings{CJ93, title={Term Rewriting}, editor={H. Comon and J.-P. Jouannaud}, series= lncs, PUBLISHER=springer, year={1993}, volume={909}} @Proceedings{WGH96, editor = "J. von Wright and J. Grundy and J. Harrison", title = "Proceedings of {TPHOL}'96", series = lncs, volume = 1125, year = 1996, publisher =springer} @Proceedings{lfcs94, title = "Proceedings of LFCS'94", year = {1994}, editor= {A. Nerode and Y.N. Matiyasevich}, volume = {813}, series = lncs, publisher = springer} @Proceedings{DGT96:pe, title = "Partial Evaluation", year = 1996, editor = "O. Danvy and R. Gl{\"u}ck and P. Thiemann", volume = "1110", series = lncs, publisher = springer} @inproceedings{ longo95logic, author = "Longo and Milsted and Soloviev", title = "A Logic of Subtyping", booktitle = "{LICS}: {IEEE} Symposium on Logic in Computer Science", year = "1995" }