@article{aba99:jacm, author="M. Abadi", title="Secrecy by Typing in Security Protocols", journal = jacm, volume = "46", year = "1999", pages = "749--786", number = "5", month = sep} @Article{AB03:tcs, author = "M. Abadi and B. Blanchet", title = "Secrecy Types for Asymmetric Communication", journal = tcs, volume = "298", year = "2003", number = "3", pages = "387--415", month=apr} @Article{AN96:tse, title = "Prudent Engineering Practice for Cryptographic Protocols", author = "M. Abadi and R. M. Needham", journal = tse, pages = "6--15", month = jan, year = "1996", volume = "22", number = "1", } @Article{AR02:jcrypt, author = "M. Abadi and P. Rogaway", title = "Reconciling two views of cryptography (The computational soundness of formal encryption)", journal = "Journal of Cryptology", volume = "15", year = "2002", pages = "103--127", number = "2"} @Article{BAN90:acm, author = "M. Burrows and M. Abadi and R. Needham", title = "A Logic of Authentication", journal = "ACM Transactions on Computer Systems", volume = "8", number = "1", pages = "18--36", month = feb, year = "1990"} @article{abe04:rairo, author={A. Abel}, title={Termination checking with types}, journal={RAIRO-- Theoretical Informatics and Applications}, year={2004}, volume=38, pages={277-320}, month=oct} @article{AA02:jfp, author={A. Abel and T. Altenkirch}, title={A predicative analysis of structural recursion}, journal=jfp, volume=12, number=1, pages={1--41}, month=jan, year={2002}} @Article{AC93:toplas, author = "R. M. Amadio and L. Cardelli", title = "Subtyping Recursive Types", journal = toplas, volume = "15", number = "4", pages = "575--631", month=sep, year = "1993"} @Article{AMcA01:toplas, author = "A.W. Appel and D. McAllester", title = "An indexed model of recursive types for foundational proof-carrying code", journal = toplas, volume = "23", number = "5", pages = "657--683", month = sep, year = "2001"} @article{AC03:jar, title={Heap-Bound Assembly Language}, author={D. Aspinall and A. Compagnoni}, year={2003}, journal=jar} @article{AHMP92:jar, author="A. Avron and F. Honsell and I. Mason and R. Pollack", title="Using Typed Lambda Calculus to Implement Formal Systems on a Machine", journal = "Journal of Automated Reasoning", year = "1992", volume = "9", pages = "309-352" } @article{bac89:fac, author={R. Backhouse and P. Chisholm and G. Malcolm}, Title={Do-it-yourself type theory}, journal={Formal Aspects of Computing}, Volume={1}, pages={19--84}, year={1989}} @Article{BCM88:part2, author = "R. Backhouse and P. Chisholm and G. Malcolm", title = "Do-It-Yourself Type Theory (Part {II})", journal = "BEATCS: Bulletin of the European Association for Theoretical Computer Science", volume = "35", year = "1988", pages={205-244}} @Article{BCM88:part1, author = "R. Backhouse and P. Chisholm and G. Malcolm", title = "Do-it-yourself Type Theory (Part {I})", journal = "BEATCS: Bulletin of the European Association for Theoretical Computer Science", volume = "34", pages={68-110}, year = "1988", } @article{bak97:apal, title={Comparing cubes of typed and type assignment systems}, author={Bakel, S. van and Liquori, L. and Ronchi della Rocca, S. and Urzyczyn, P.}, pages={267--303}, journal=apal, year=1997, volume=86, month=jul, number=3 } @article{bal93:toplas, title = "What's In a Region? {Or} Computing Control Dependence Regions In Near-Linear Time for Reducible Control Flow", author = "T. Ball", journal = "ACM Letters on Programming Languages and Systems", pages = "1--16", year = "1993", month = mar # "--" # dec, volume = "2", number = "1--4", } @article{BN05:jfp, author={A. Banerjee and D. Naumann}, title={Stack-based Access Control for Secure Information Flow}, year={2005}, journal=jfp, volume=15, issue=2, month=mar, pages={131-177}} @Article{BB95:apal, title={A strong normalization result for classical logic}, author={F. Barbanera and S. Berardi}, pages={99--116}, journal=apal, month=dec, year=1995, volume=76, number=2} @Article{BB96:ic, title={A Symmetric Lambda Calculus for Classical Program Extraction}, author={F. Barbanera and S. Berardi}, pages={103--117}, journal=ic, month=mar, year=1996, volume=125, number=2} @Article{BB96:jfp, title={Proof-irrelevance out of excluded-middle and choice in the calculus of constructions}, author={F. Barbanera and S. Berardi}, pages={519--525}, journal=jfp, month=may, year=1996, volume=6, number=3 } @article {BDL95:ic, title = {Intersection and Union Types: Syntax and Semantics}, author = {F. Barbanera and M. Dezani-Ciancaglini and U. de'Liguoro}, pages = {202--230}, journal = ic, year = 1995, volume = 119, number = 2 } @Article{BF96:tcs, title={Intersection type assignment systems with higher-order algebraic rewriting}, author={F. Barbanera and M. Fern{\'a}ndez}, pages={173--207}, journal=tcs, month= dec, year=1996, volume=170, number={1--2}} @article{BFG97:jfp, author={F. Barbanera and M. Fern{\'a}ndez and H. Geuvers}, title={Modularity of strong normalisation and confluence in the algebraic $\lambda$-cube}, year={1997}, month=nov, journal=jfp, volume={7}, number={6}, pages={613--660}} @article{henk91:jfp, author = "H. Barendregt", title = "Introduction to {G}eneralised {T}ype {S}ystems", journal =jfp, volume = 1, number = 2, pages = "125--154", year = 1991, month = {April} } @Article{henk97:bsl, title={The Impact of the Lambda Calculus in Logic and Computer Science}, author={H. Barendregt}, pages={181--215}, journal=bsl, year=1997, month=jun, volume=3, number=2} @article{bas+03:jar, author={D. Basin and S. Friedrich and M. Gawkowski}, title={{Bytecode Verification by Model Checking}}, journal=jar, volume = "30", number = "3-4", pages = "399-444", month = dec, year = "2003"} @article{BMP03:jsac, author ="G. Bella and F. Massacci and L.C. Paulson", title="Verifying the SET registration protocols", journal="IEEE Journal on Selected Areas in Communications", volume={21}, issue={1}, year={2003}, pages={77-87}} @Article{BBP98:jfp, title={Computational types from a logical perspective}, author={P.N. Benton and G.M. Bierman and V.C.V. de Paiva}, journal=jfp, year={1998}, volume={8}, number=2, month=mar} @Article{ben93:ic, title={Typing in Pure Type Systems}, author={Benthem Jutting, L.S. van}, pages={30-41}, journal=ic, month=jul, year=1993, volume=105, number=1} @article{BSS01:jar, author={U. Berger and H. Schwichtenberg and M. Seisenberger}, title={{The Warshall Algorithm and Dickson's Lemma: Two Examples of Realistic Program Extraction}}, journal=jar, volume=26, number=2, pages= {205--221}, year={2001}} @article{BK86:jcss, author={J. Bergstra and J.W. Klop}, title={Conditional rewrite rules: confluence and termination}, journal=jcss, pages={323-362}, volume={32}, year={1986}} @article{BFS98:tapos, author={E. Bertino and E. Ferrari and P. Samarati}, title={Mandatory Security and Object-Oriented Systems: A Multilevel Entity Model and its Mapping onto a Single-Level Object Model}, pages={183--204}, journal=tapos, year=1998, volume=4, number=3} @article{BJLMT01:jcs, title={Model checking security properties of control flow graphs}, author={F. Besson and T. Jensen and D. Le M\'etayer and T.Thorn}, journal=jcs, volume=9, issue=3, pages={217-250}, year={2001}} @ARTICLE{BeJePi06TCS, AUTHOR = {F.~Besson and T.~Jensen and D~Pichardie}, TITLE = {{Proof-Carrying Code from Certified Abstract Interpretation and Fixpoint Compression}}, JOURNAL = tcs, YEAR = {2006}, PUBLISHER = {Elsevier}, NOTE = {To appear} } @article{BR96:fi, author={I. Bethke and P. Rodenburg}, title={Equational Constructor Induction}, journal=fi, pages={1--16}, volume={25}, number={1}, year={1996}} @article{lan+02:jcs, author={P. Bieber and J. Cazin and V. Wiels and G. Zanon and P. Girard and J.-L. Lanet}, title="{Checking Secure Interactions of Smart Card Applets: Extended version}", journal=jcs, volume=10, issue=4, year=2002, pages={369-398}} @Article{bla03:toplas, author = "B. Blanchet", title = "Escape analysis for Java: {Theory} and practice", journal = toplas, volume = "25", number = "6", pages = "713--775", month = nov, year = "2003", } @article{bla05:mscs, author = {F. Blanqui}, title = "Definitions by rewriting in the Calculus of Constructions", journal=mscs, number={1}, year = 2005, volume = 15, month=feb, pages = {37--92}} @article{BJO02:tcs, author = {F. Blanqui and J.-P. Jouannaud and M. Okada}, title = {Inductive {D}ata {T}ype {S}ystems}, journal=tcs, number={1/2}, year = 2002, volume = 272, month=feb, pages = {41--68}} @article{BFT99:tse, author = {Blasio, P. di and Fisher, K. and Talcott, C.}, title = {A Control-Flow Analysis for a Calculus of Concurrent Objects}, year = 1999, journal=tse} @Article{Blum95, author = "M. Blum and S. Kannan", title = "Designing Programs That Check Their Work", journal = "Journal of the ACM", month = jan, year = "1995", volume = "42", number = "1", pages = "269--91", } @article{BC02:tcs, author = {G. Boudol and I. Castellani}, title = {Noninterference for Concurrent Programs and Thread Systems}, journal = tcs, volume = 281, number = {1}, year = 2002, pages = {109-130}, note = {Preliminary version available as INRIA Research report 4254}} @Article{bou97:jsc, author = {A. Bouhoula}, title = {Automated Theorem Proving by Test Set Induction}, journal = {Journal of Symbolic Computation}, year = 1997, volume = 23, pages = {47-77}, number=1, month=jan} @Article{bou96:tcs, author = {A. Bouhoula}, title = {Using induction and rewriting to verify and complete parameterized specifications}, journal = tcs, year = 1996, number = 170, volume = {1-2}, pages = {245--276} } @Article{BC05:mscs, author = {A. Bove and V. Capretta}, title = {Modelling General Recursion in Type Theory}, journal = mscs, year = {2005}, month = feb, issue=1, volume = {15}, pages = {671--708} } @Article{BG95:ist, title = "A Shallow Embedding of {Z} in {HOL}", author = "J. P. Bowen and M. J. C. Gordon", journal = "Information and Software Technology", year = "1995", volume = "37", number = "5--6", pages = "269--276"} @Article{BH98:fi, author = "M. Brandt and F. Henglein", year = "1998", title = "Coinductive axiomatization of recursive type equality and subtyping", journal = "Fundamenta Informaticae", volume = "33", pages = "309--338", number=4, month=apr} @article{BCGS91:ic, author={V. Breazu-Tannen and T. Coquand and C. Gunter and A. Scedrov}, title={Inheritance as implicit coercion}, journal=ic, year={1991}, volume={93}, pages={172-221}} @article{BTG94:ic, author={V. Breazu-Tannen and J. Gallier}, title={Polymorphic rewriting conserves algebraic confluence}, journal=ic, year={1994}, volume={114}, pages={1-29}} @ARTICLE{BCHJ05:scp, AUTHOR = {C. Breunesse and N. Cata{\~n}o and M. Huisman and B. Jacobs}, TITLE = {Formal Methods for Smart Cards: an experience report}, JOURNAL = scp, YEAR = {2005}, VOLUME = 55, NUMBER = {1-3}, PAGES = {53-80}, month=mar } @article{conor:faking, author={C. McBride}, title={{Faking It (Simulating Dependent Types in Haskell)}}, journal=jfp, year={2002}, note={To appear}} @article (BCP99:ic, author = "K.B. Bruce and L. Cardelli and B.C. Pierce", title = "Comparing Object Encodings", journal = "Information and Computation", year = "1999", note = "To appear in a special issue with papers from {\em Theoretical Aspects of Computer Software (TACS)}") @article{jml:sttt, author={L. Burdy and Y. Cheon and D.R. Cok and M.D. Ernst and J. Kiniry and G.T. Leavens and K.R.M. Leino and E. Poll}, title={{An overview of JML tools and applications}}, journal=sttt, year={2005}} @Article{BL84:ic, author = "R. Burstall and B. Lampson", title = "A Kernel Language for Abstract Data Types and Modules", journal = ic, volume = "76", number = "2/3", year = "1984"} @Article{cac+05:tcs, author = "D.~Cachera and T.~Jensen and D.~Pichardie and V.~Rusu", title = "Extracting a Data Flow Analyser in Constructive Logic", journal = tcs, volume = "342", year = "2005", note="To appear"} @Article{CL01:jar, author = {P. Callaghan and Z. Luo}, title = {{Plastic: An implementation of typed LF with coercive subtyping and universes}}, journal = jar, year = {2001}, volume=27, issue=1, pages={3--27}} @article{cap05:lmcs, author = "Venanzio Capretta", title = "General Recursion via Coinductive Types", journal="Logical Methods in Computer Science", volume = 1, number = 2, year = 2005, pages = {1--18}} @article{car96:acmcs, title={Type Systems}, author={L. Cardelli}, journal=acmcs, pages={263--264}, month=mar, year=1996, volume=28, number=1} @Article{car88:ic, author = "L. Cardelli", title = "A Semantics of Multiple Inheritance", journal = ic, volume = "76", number = "2/3", month = feb # "/" # mar, year = "1988", pages = "138--164", note = "Preliminary version in the 1984 Semantics of Data Types Symposium, LNCS 173, pages 51--66"} @article (CL91:jfp, author = "L. Cardelli and G. Longo", title = "A semantic basis for {Q}uest", journal = "Journal of Functional Programming", year = "1991", month = "October", volume = "1", number = "4", pages = "417--458") @ARTICLE{CW85:acmcs, AUTHOR = "L. Cardelli and P. Wegner", TITLE = "On understanding types, data abstraction and polymorphism", JOURNAL = acmcs, month=dec, year=1985, volume=17, number=4, PAGES = "471--522"} @Article{CF96:acmcs, author = "R. Cartwright and M. Felleisen", title = "Program Verification Through Soft Typing", journal = acmcs, volume = "28", number = "2", pages = "349--351", month = jun, year = "1996" } @Article{CGL95:ic, title={A Calculus for Overloaded Functions with Subtyping}, author={G. Castagna and G. Ghelli and G. Longo}, pages={115--135}, journal=ic, month= feb, year=1995, volume=117, number=1} @Article{CC01:ic, title={Dependent types with subtyping and late-bound overloading}, author={G. Castagna and G. Chen}, journal=ic, year={2001}, volume=168, issue=1, pages={1-67}} @Article{CK01:hosc, author = "W.-N. Chin and S.-C. Khoo", title = "Calculating Sized Types", journal = hosc, volume = "14", number = "2--3", pages = "261--300", month = sep, year = "2001" } @ARTICLE{chu32:am , AUTHOR = "A. Church" , TITLE = "A set of postulates for the foundation of logic" , JOURNAL = AoM , VOLUME = 33 , PAGES = "346--366" , YEAR = 1932 } @ARTICLE{chu33:am , AUTHOR = "A. Church" , TITLE = "A set of postulates for the foundation of logic" , JOURNAL = AoM , VOLUME = 34 , PAGES = "839--864" , YEAR = 1933 } @ARTICLE{chu40:jsl , AUTHOR = "A. Church" , TITLE = "A formulation of the simple theory of types" , JOURNAL = jsl , VOLUME = 5 , PAGES = "414--432" , YEAR = 1940 } @Article{CGL94:toplas, author = "E. M. Clarke and O. Grumberg and D. E. Long", title = "Model Checking and Abstraction", journal = toplas, volume = "16", number = "5", pages = "1512--1542", month = sep, year = "1994" } @Article{cog04:cpe, author = "A. Coglio", title = "Simple verification technique for complex {Java} bytecode subroutines", journal = "Concurrency and Computation: Prac\-tice and Experience", volume = "16", number = "7", pages = "647--670", year = "2004" } @Article{CG01:ccpe, author = {A. Coglio and A. Goldberg}, title = {Type Safety in the {JVM}: Some Problems in {Java} 2 {SDK} 1.2 and Proposed Solutions}, journal = {Concurrency and Computation: Practice and Experience}, year = {2001}, volume = {13}, number = {13}, pages = {1153--1171}, month = nov, } @article (adriana96:mscs, author = "A. Compagnoni and B. Pierce" , title = "Intersection Types and Multiple Inheritance", pages = {469--501}, journal = mscs, month = oct, year = 1996, volume = 6, number = 5 ) @article (compose98:sope, title={Tempo: Specializing Systems Applications and Beyond}, author={C. Consel and L. Hornof and R. Marlet and G. Muller and S. Thibault and E.- N. Volanschi}, journal=acmcs, volume=30, number=3, month=sep, year=1998, note={Symposium on Partial Evaluation (SOPE '98)}) @Article{CS93:tcs, title={Computational foundations of basic recursive function theory}, author={R. L. Constable and S. F. Smith}, pages={89--112}, journal=tcs, year=1993, month= dec, volume=121, number={1--2} } @article {CD78:aml, author = "M. Coppo and M. Dezani-Ciancaglini", title = "A New Type-Assignment for $\lambda$-Terms", journal = "Archiv f{\"u}r Mathematische Logik", volume = 19, pages = "139-156", year = "1978"} @Article{coq92:bit, author = "T. Coquand", title = "The paradox of trees in type theory", journal = "BIT", volume = "32", number = "1", pages = "10--14", year = "1992"} @Article{coq95:jsl, title={A Semantics of Evidence for Classical Arithmetic}, author={T. Coquand}, pages={325--337}, journal=jsl, year=1995, volume=60, number=1} @Article{CH94:jfp, title={A-translation and looping combinators in pure type systems}, author={T. Coquand and H. Herbelin}, pages={77--88}, journal=jfp, month=jan, year=1994, volume=4, number=1 } @Article{DCK94:mscs, title={Simulating expansions without expansions}, author={R. Di Cosmo and D. Kesner}, pages={315--362}, journal=mscs, month=sep, year=1994, volume=4, number=3} @Article{DCK96:tcs, title={Combining algebraic rewriting, extensional lambda calculi, and fixpoints}, author={R. Di Cosmo and D. Kesner}, pages={201--220}, journal=tcs, month=dec, year=1996, volume=169, number=2} @Article{thierry96:scp, title={An algorithm for type-checking dependent types}, author={T. Coquand}, pages={167--177}, journal=scp, month=may, year=1996, volume=26, number={1--3}} @article{CH88:ic, author="T. Coquand and G. Huet", title={{The Calculus of Constructions}}, journal=ic, volume=76, number="2/3", pages="95--120", month={February/March}, year=1988 } @Article{CH85:jsc, author={T. Coquand and G. Huet}, title={A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction}, journal=jsc, year=1985, volume=1, number=3, pages={323--328}, month=sep } @article{cou96:acmcs, author = {Cousot, P{.}}, title = {Program Analysis: The Abstract Interpretation Perspective}, journal = acmcs, volume = {28A}, number = {4es}, month = dec, year = 1996, pages = {165-es}} @Article{CDS98:mscs, title = "Normalization and the {Yoneda} embedding", author = "D. {\v{C}}ubri{\'c} and P. Dybjer and P. Scott", pages = "153--192", journal = mscs, month = apr, year = "1998", volume = "8", number = "2"} @article{DOB98:njc, author={O.-J. Dahl and O. Owe and T.J. Bastiansen}, title={Subtyping and Constructive Specification}, journal=njc, volume= 5, number={1}, pages={}, year={1998}, month={Spring}} @Article{den76:cacm, author = "D.E. Denning", title = "A Lattice Model of Secure Information Flow", journal = cacm, volume = "19", number = "5", pages = "236--243", month = may, year = "1976"} @Article{DD77:cacm, author = "D.E. Denning and P.J. Denning", title = "Certification of Programs for Secure Information Flow", journal = cacm, volume = "20", number = "7", pages = "504--513", month = jul, year = "1977" } @Article{DD85:toplas, author = "J. Donahue and A. Demers", title = "Data Types Are Values", journal = toplas, volume = "7", number = "3", pages = "426--445", month = jul, year = "1985"} @Article{DHK03:jar, title = "Theorem Proving Modulo", author = "G. Dowek and T. Hardin and C. Kirchner", journal = "Journal of Automated Reasoning", year = "2003", number = "1", volume = "31", pages = "33--72" } @Article{DR94a:mscs, title = "Sketches and computation---{I}: basic definitions and static evaluation", author = "D. Duval and J.-C. Reynaud", pages = "185--238", journal = mscs, month = jun, year = "1994", volume = "4", number = "2" } @Article{DR94b:mscs, title = "Sketches and computation---{I}: dynamic evaluation and applications", author = "D. Duval and J.-C. Reynaud", pages = "239--271", journal = mscs, month = jun, year = "1994", volume = "4", number = "2" } @ARTICLE{dyb94:fac, AUTHOR = "P. Dybjer", TITLE = "Inductive Families", JOURNAL = fac, VOLUME = "6", PAGES = "440-465", YEAR = 1994} @ARTICLE{dyb97:tcs, AUTHOR = "P. Dybjer", TITLE ={{Representing inductively defined sets by well-orderings in Martin-L{\"o}f's type theory}}, journal=tcs, pages={329--335}, month= apr, year=1997, volume=176, number={1--2}} @ARTICLE{dyb00:jsl, AUTHOR = "P. Dybjer", TITLE ={A general formulation of simultaneous inductive-recursive definitions in type theory}, journal=jsl, year={2000}, Volume={65}, Number={2}, pages={525-549}, month=jun} @Article{DMP95:lasc, title={The essence of eta-expansion in partial evaluation}, author={O. Danvy and K. Malmkjaer and J. Palsberg}, journal=lasc, pages={209--227}, year=1995, volume=8, number=3 } @Article{DMP96:toplas, title={Eta-Expansion Does The Trick}, author={O. Danvy and K. Malmkjaer and J. Palsberg}, journal=toplas, pages={730--751}, month=nov, year=1996, volume=18, number=6 } @Article{DN95:jsl, title={Storage Operators and Directed Lambda-Calculus}, author={R. David and K. Nour}, pages={1054--1086}, journal=jsl, year=1995, month=dec, volume=60, number=4 } @article{DM05:jot, author = {Dietl, W. and M\"uller, P.}, title = {Universes: Lightweight Ownership for {JML}}, journal = {Journal of Object Technology (JOT)}, year = {2005}, note = {To appear} } @article{dou92:ic, author={D. Dougherty}, title={Adding algebraic rewriting to the untyped lambda calculus}, journal=ic, year={1992}, volume={101}, month=dec, number=2, pages={251-267}} @Article{dow93:jlc, title={A Complete Proof Synthesis Method for the Cube of Type Systems}, author={G. Dowek}, pages={287--315}, journal=jlc, year=1993, volume=3, number=3} @article{fef64:jsl, author={S. Feferman}, title={Solomon Systems of predicative analysis}, journal=jsl, pages={1--30}, year={1964}, volume=29} @article{FG97:tse, title={The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties}, author={R. Focardi and R. Gorrieri}, journal=tse, volume=23, number=9, month=sep, year=1997} @Article{FC00:tosem, author = "P. Fong and R. Cameron", title = "Proof linking: modular verification of mobile programs in the presence of lazy, dynamic linking", journal = "ACM Transactions on Software Engineering and Methodology", volume = "9", number = "4", pages = "379--409", month = oct, year = "2000"} @Article{FG02:toplas, author = "C. Fournet and A.D. Gordon", title = "Stack inspection: {Theory} and variants", journal = toplas, volume = "25", number = "3", pages = "360--399", month = may, year = "2003"} @Article{FM99:toplas, author = "S. N. Freund and J. C. Mitchell", title = "The type system for object initialization in the {Java} bytecode language", journal = toplas, volume = "21", number = "6", pages = "1196--1250", month = nov, year = "1999"} @Article{FM03:jar, author = "S. N. Freund and J. C. Mitchell", title = "{A Type System for the Java Bytecode Language and Verifier}", journal = jar, volume = "30", number = "3-4", pages = "271-321", month = dec, year = "2003"} @article{GN91:jfp, author={H. Geuvers and M.J. Nederhof}, title={A modular proof of strong normalisation for the {C}alculus of {C}onstructions}, journal=jfp, volume={1}, number={2}, month=apr, pages={155-189}, year={1991}} @Article{ghe97:ic, title={Termination of System {$F$}-bounded: A Complete Proof}, author={G. Ghelli}, pages={39--56}, journal=ic, month=nov, year=1997, volume=139, number=1} @Article{GJ97:lasc, author = "R. Gl{\"u}ck and J. J{\o}rgensen", title = "An Automatic Program Generator for Multi-Level Specialization", journal = "Lisp and Symbolic Computation", volume = "10", number = "2", pages = "113--158", month = jul, year = "1997"} @ARTICLE{GD94:mscs, AUTHOR = "J. Goguen and R. Diaconescu", TITLE = "An {O}xford survey of order sorted algebra", JOURNAL = mscs, VOLUME = "4", YEAR = 1994, PAGES = "363--392", month=sep, number=3} @article{GM85:hjm, author={J. Goguen and J. Meseguer}, title={Completeness of Many-Sorted Equational Logic}, journal={Houston Journal of Mathematics}, Volume=11, number=3, pages={307-334}, year={1985}} @Article{GM92:tcs, author = "J. Goguen and J. Meseguer", title = "Order-Sorted Algebra {I}: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations", journal = tcs, volume = "105", number={2}, pages={216-273}, year = "1992", } @Article{GM93:ic, title = "Order-Sorted Algebra Solves the Constructor-Selector, Multiple Representation, and Coercion Problems", author = "J. Meseguer and J. Goguen", pages = "114--158", journal = ic, month = mar, year = "1993", volume = "103", number = "1", } @Article{GL94:toplas, title = "Model Checking and Modular Verification", author = "O. Grumberg and D.E. Long", journal = toplas, pages = "843--871", month = may, year = "1994", volume = "16", number = "3", } @Article{HDM93:jfp, title={Typing first-class continuations in {ML}}, author={R. Harper and B.F. Duba and D. MacQueen}, pages={465--484}, journal=jfp, month=oct, year=1993, volume=3, number=4 } @Article{HHP93:jacm, title={A Framework for Defining Logics}, author={R. Harper and F. Honsell and G. Plotkin}, pages={143--184}, journal=jacm, month=jan, year=1993, volume=40, number=1} @Article{HL93:lasc, author = "R. Harper and M. Lillibridge", title = "Polymorphic type assignment and CPS conversion", journal = LASC, year = 1993, volume = 6, number = 4, pages = "361-380" } @article(HM93:toplas, author="Harper, R. and Mitchell, J.C.", Title="On the type structure of {Standard ML}", Journal=toplas, volume="15", Number="2", Year="1993", pages="211--252", month=apr) @article{har99:spe, title={{LETOS} - a lightweight execution tool for operational semantics}, author={P. Hartel}, journal=spe, year={1999}, month=sep, volume={29}, number={5}, pages={1379--1416}} @article{HM01:acmcs, author={P. Hartel and L. Moreau}, title={{Formalizing the Safety of Java, the Java Virtual Machine and Java Card}}, journal=acmcs, year=2001, volume={33}, number={4}, month=dec, pages={517-558}} @Article{john98:sope, author={J. Hatcliff}, title={Foundations of Partial Evaluation of Functional Programs with Computational Effects}, journal=acmcs, note={Special issue on Partial Evaluation.}, editors={O. Danvy and R. Gl{\"u}ck and P. Thiemann}, year={1998}} @Article{HD97:mscs, author = {J. Hatcliff and O. Danvy}, title = "A Computational Formalization for Partial Evaluation", pages={507--541}, journal=mscs, month=oct, year=1997, volume=7, number=5 } @article{hoa69:cacm, author = {C.A.R. Hoare}, title = {An axiomatic basis for computer programming}, journal = {Communications of the ACM}, volume = 12, year = 1969, pages = {576--583} } @Article{martin95:mscs, title={Sound and complete axiomatisations of call-by-balue control operators}, author={M. Hofmann}, pages={461--482}, journal=mscs, month=dec, year=1995, volume=5, number=4} @article (HP95:jfp, author = "M. Hofmann and B. Pierce" , title = "A Unifying Type-Theoretic Framework for Objects", journal = jfp, pages={593-635}, volume={5}, number={4}, year={1995} ) @article{hor97:toplas, author = "S. Horwitz", title = "Precise Flow-Insensitive May-Alias Analysis is {NP-Hard}", journal = toplas, volume = "19", number = "1", pages = "1--6", month = jan, year = "1997"} @Article{how96:ic, title={Proving Congruence of Bisimulation in Functional Programming Languages}, author={D.J. Howe}, pages={103--112}, journal=ic, month=feb, year=1996, volume=124, number=2} @Article{hue75:tcs, title={A Unification Algorithm for Typed {$\lambda$}-Calculus}, author={G. Huet}, pages={27--57}, journal=tcs, year=1975, month=jun, volume=1, number=1} @Article{hue80:jacm, title={Confluent Reductions: Abstract Properties and Application to Term Rewriting Systems}, author={G. Huet}, pages={797--821}, journal=jacm, month=oct, year=1980, volume=27, number=4, } @Article{bart96:jfp, author={B. Jacobs}, title={On cubism}, pages={379--391}, journal=jfp, month=may, year=1996, volume=6, number=3 } @Article{bart03:jlap, author={B. Jacobs}, title={Weakest Precondition Reasoning for Java Programs with JML Annotations}, journal=jlap, year={2004}, volume=58, issue={1/2}, pages={61-88}} @Article{JG95:jfp, title={The Virtues of Eta-expansion}, author={C.B. Jay and N. Ghani}, pages={135--154}, journal=jfp, month=apr, year=1995, volume=5, number=2 } @article{JCYC04:jss, author = "J.W. Jo and B.M. Chang and K. Yi and K.M. Choe", title = "An uncaught exception analysis for {Java}", journal = "Journal of systems and software", volume = "72", number = "1", pages = "59--69", year = "2004", } @article{joa03:ic, author={F. Joachimski}, title={{Syntactic Analysis of eta-Expansions in Pure Type Systems}}, journal=ic, year={2003}, note={To appear}} @Article{jon83:toplas, author = "C. B. Jones", title = "Tentative steps towards a development method for interfering programs", journal = toplas, year = "1983", month = oct, volume = "5", number = "4", pages = "596--619", } @article{JL00:scp, author = "R. Joshi and K. R. M. Leino", title = "A Semantic Approach to Secure Information Flow", journal = "Science of Computer Programming", year = 2000, volume = "37", number = "1--3", pages = "113--138", publisher = "Elsevier" } @Article{JL82:ipl, title={On multiset orderings}, author={J.-P. Jouannaud and P. Lescanne}, pages={57--63}, journal=ipl, year=1982, month=sep, volume=15, number=2 } @Article{JO97:tcs, title={Abstract data type systems}, author={J.-P. Jouannaud and M. Okada}, pages={349--391}, journal=tcs, year=1997, volume=173, month=feb, number=2} @Article{KN96:jfp, title={Canonical typing and {$\Pi$}-conversion in the {Barendregt Cube}}, author={F. Kamareddine and R. Nederpelt}, pages={245--267}, journal=jfp, month=mar, year=1996, volume=6, number=2 } @Article{KPT96:ic, title = "A Typed Pattern Calculus", author = "D. Kesner and L. Puel and V. Tannen", pages = "32--61", journal = ic, month = "10", year = "1996", volume = "124", number = "1"} @Article{KN01:cpe, author = "G. Klein and T. Nipkow", title = "Verified lightweight bytecode verification", journal = "Concurrency and Computation: Practice and Experience", volume = "13", number = "13", pages = "1133--1151", month = nov, year = "2001" } @article{KN02:tcs, title={Verified Bytecode Verifiers}, author={G. Klein and T. Nipkow}, journal=tcs, year={2002}, pages="583--626", volume={298}, number={3}, month=apr} @Article{KS04:jlap, author = {G. Klein and M. Strecker}, title = {Verified {B}ytecode {V}erification and {T}ype-{C}ertifying {C}ompilation}, journal =jlap, year={2004}, volume=58, issue={1/2}, pages={27-60} } @article{KW03:jar, author={G. Klein and M. Wildmoser}, title={Verified Bytecode Subroutines}, journal=jar, volume = "30", number = "3-4", pages = "363--398", month = dec, year = "2003"} @Article{KPS95:mscs, title = "Efficient recursive subtyping", author = "D. Kozen and J. Palsberg and M. Schwartzback", pages = "113--125", journal = mscs, month = mar, year = "1995", volume = "5", number = "1" } @Article{koz83:tcs, author = "D. Kozen", title = "Results on the propositional mu-calculus", journal = "Theoretical Computer Science", year = "1983", volume = "27", pages = "333--354", } @article{KD98:njc, author={B. Kristoffersen and O.-J. Dahl}, title={On Introducing Higher Order Functions in {ABEL}}, journal=njc, volume= 5, number={1}, pages={}, year={1998}, month={Spring}} @Article{kri94:apal, title={Classical logic, storage operators and second-order lambda-calculus}, author={J.-L. Krivine}, pages={53--78}, journal=apal, month=jun, year=1994, volume=68, number=1} @Article{lam68:mst, title={Deductive Systems and Categories {I}. {Syntactic} Calculus and Residuated Categories}, author={J. Lambek}, journal=mst, pages={287--318}, year=1968, volume=2, number=4} @Article{LB88:ic, author = "B. Lampson and R. Burstall", title = "Pebble, a Kernel Language for Modules and Abstract Data Types", journal = "Information and Computation", volume = "76", number = "2/3", month = feb # "/" # mar, year = "1988", pages = "278--346", } @Article{lav91:jsc, author={A. Laville}, title={Comparison of Priority Rules in Pattern Matching and Term Rewriting}, journal=jsc, year=1991, volume=11, number=4, pages={321--348}, month=apr } @article{lan02:tcs, title={{A Type System for {JVM} Threads}}, author={C. Laneve}, journal=tcs, volume = "290", number = "1", pages = "741--778", month = oct, year = "2002"} @ARTICLE{law64:pnas, AUTHOR = "F.W. Lawvere", TITLE = "An elementary theory of the category of sets", JOURNAL = pnas, VOLUME = 52, YEAR = 1964, PAGES = "1506--1511"} @ARTICLE{law69:dia, AUTHOR = "F.W. Lawvere", TITLE = "Ajointness in foundations", JOURNAL = "Dialectica", VOLUME = 23, YEAR = 1969, PAGES = "281--296"} @article{LMS05:scp, title="Generating error traces from verification-condition counterexamples", journal=scp, volume=55, issue="1-3", month=mar, pages="209-226", author="K.R.M. Leino and T. Millstein and J.B. Saxe", year="2005"} @Article{lei85:jsl, author = "Leivant, D.", title = "Syntactic Translations and Provably Recursive Functions", journal = jsl, year = "1985", volume = "50", number = "3", pages = "682--688" } @article{ler00:jfp, author={X. Leroy}, title={A modular module system}, journal=jfp, volume= 10, number=3, pages={269--303}, month=may, year=2000} @Article{ler02:spe, author = "X. Leroy", title = "Bytecode verification on {Java} smart cards", journal =spe, volume = "32", number = "4", pages = "319--340", day = "10", month = apr, year = "2002" } PDF DOI resolver @Article{ler03:jar, author = "X. Leroy", title = "{Java bytecode verification: algorithms and formalizations}", journal = jar, volume = "30", number = "3-4", pages = "235-269", month = dec, year = "2003"} @Article{lev76:tcs, author={J.-J. L{\'e}vy}, title={An algebraic interpretation of the $\lambda\beta\kappa$-calculus and a labelled $\lambda$-calculus}, pages={97--114}, journal=tcs, year=1976, volume=2} @Article{loi+95:fmsd, author = "C. Loiseaux and S. Graf and J. Sifakis and A. Bouajjani and S. Bensalem", title = "Property Preserving Abstractions for the Verification of Concurrent Systems", journal = "Formal Methods in System Design: An International Journal", publisher = kluwer, year = "1995", volume = "6", number = "1", month = jan, pages = "11--44", } @Article{LM91:mscs, title={Constructive natural deduction and its `{$\omega$}-set' interpretation}, author={G. Longo and E. Moggi}, pages={215--254}, journal=mscs, month=jul, year=1991, volume=1, number=2 } @article{luo99:jlc, author = "Z. Luo", title = "Coercive Subtyping", journal=jlc, year={1999}, pages={105--130}, volume={9}, number={1}, month=feb} @article{McBMcK04:jfp, author={McBride, C. and McKinna, J. }, title={The View from the Left}, journal=jfp, pages={69-111}, volume=14, issue=1, year={2004}} @article{jamesrandy:jar, author={McKinna, J. and Pollack, R.}, title={Some Lambda Calculus and Type Theory Formalized}, volume=23, number=3, pages={373--409}, year={1999}, journal=jar}} @ARTICLE{man75:lms, author={C. Mann}, title={The connection between equivalences of proofs and cartesian closed categories}, journal={Proceedings of the London Mathematical Society}, volume={31}, pages={289--310}, year={1975}} @Article{MS03:jcs, title = "A Unifying Approach to the Security of Distributed and Multi-Threaded Programs", author = "H. Mantel and A. Sabelfeld", journal = "Journal of Computer Security", year = "2003", number = "4", volume = "11", pages = "615--676", } @Article{MPU03:jlap, author={C. March{\'e} and C. Paulin-Mohring and X. Urbain}, title="{The Krakatoa tool for certification of Java/JavaCard Programs annotated with JML Annotations}", journal=jlap, year={2004}, volume=58, issue={1/2}, pages={89-106}} @Article{mea96:jlp, author = {C. Meadows}, title = {{The NRL Protocol Analyzer: An Overview}}, journal = jlp, year = {1996}, volume = {26}, number = {2}, pages = {113-131}, month = feb} @Article{men91:apal, author = "N. P. Mendler", title = "Inductive Types and Type Constraints in the Second-order Lambda Calculus", journal = apal, year = "1991", volume = "51", number = "1-2", month = mar, pages = "159--172"} @Article{mil78:jcss, author = "R. Milner", title = "A Theory of Type Polymorphism in Programming", journal = jcss, volume = "17", pages = "348--375", year = "1978" } @Article{mog91:ic, author = "E. Moggi", title = "Notions of Computations and Monads", journal = ic, year = 1991, volume = 93, number=1, month=jul, pages = "55-92" } @Article{mor+99:toplas, title = "From System{~F} to Typed Assembly Language", author = "G. Morrisett and D. Walker and K. Crary and N. Glew", journal = toplas, publisher = "ACM Press", year = "1999", volume = "21", month = nov, number = "3", pages = "527--568" } @Article{nau65:bit, author = "P. Naur", title = "Checking of operand types in ALGOL compilers", journal ={BIT}, year = 1965, volume = 5, pages = "151--163" } @article{nec94:rmn, author = "Nechaev, V. I.", title = "Complexity of a determinate algorithm for the discrete logarithm", journal = "Mathematical Notes", volume = 55, number = 2, pages = "165--172", year = 1994} @Article{NKK02:jar, AUTHOR = {Q.-H. Nguyen and C. Kirchner and H. Kirchner}, TITLE = {External rewriting for skeptical proof assistants}, JOURNAL = jar, VOLUME = {29}, NUMBER = {3-4}, PAGES = {309--336}, YEAR = {2002} } @Article{nor88:bit, author = "B. Nordstr{\"o}m", title = "Terminating general recursion", journal = "BIT", volume = "28", number = "3", pages = "605--619", year = "1988"} @article{OP97:jfp, author={P. {\O}rbaek and J. Palsberg}, title={Trust in the Lambda-calculus}, journal=jfp, volume={7}, number={6}, pages={557--591}, month=nov, year={1997}} @article{OD91:fac, author={O. Owe and O.-J. Dahl}, title={{Generator Induction in Order-Sorted Algebras}}, journal=fac, pages={2--20}, volume={3}, number={1}, year={1991}} @article{OG76:acta, author = "S. Owicki and D. Gries", title = "An axiomatic proof technique for parallel programs", year = "1976", journal= "Acta Informatica", pages = "319--340", volume=6} @Article{pal96:acmcs, title={Type Inference for Objects}, author={J. Palsberg}, journal=acmcs, pages={358--359}, month=jun, year=1996, volume=28, number=2} @Article{pal95:ic, title={Efficient Inference of Object Types}, author={J. Palsberg}, pages={198--209}, journal=ic, month=dec, year=1995, volume=123, number=2, note={Also see Erratum, Information and Computation 126(1):103--104, April 1996}} @Article{pal96:ic, title={Erratum: Efficient Inference of Object Types}, author={Jens Palsberg}, pages={103--104}, journal=ic, month= apr, year=1996, volume=126, number=1} @article{PJ97:njc, title={Type Inference with Simple Selftypes is {NP}-complete}, author={J. Palsberg and T. Jim}, journal=njc, volume={4}, number={1}, pages={259--286}, year={1997}} @article{PZ01:ic, author = "J. Palsberg and T. Zhao", title = "Efficient and Flexible Matching of Recursive Types", pages = "364-387", journal=ic, year = "2001", volume={171}, month=nov} @Article{PW93:jsc, author = "C. Paulin-Mohring and B. Werner", title = "Synthesis of {ML} Programs in the System {Coq}", journal = jsc, volume = "15", number = "5--6", pages = "607--640", year = "1993" } @Article{pau86:jsc, author={L.C. Paulson}, title={Constructing Recursion Operators in Intuitionistic Type Theory}, journal=jsc, year=1986, volume=2, number=4, pages={325--355}} @Article{pau98:jcs, author = {L.C. Paulson}, title = {The inductive approach to verifying cryptographic protocols}, journal = jcs, year = {1998}, volume = {6}, number = {1/2}, pages = {85--128} } @Article{pel86:jar, title={Seventy-Five Problems for Testing Automatic Theorem Provers}, author={F.J. Pelletier}, journal=jar, pages={191--216}, year=1986, volume=2, number=2} @article (PS97:tcs, author = "B. Pierce and M. Steffen" , title = "Higher-Order Subtyping", year = 1997, journal = "Theoretical Computer Science", volume = 176, number = "1--2", pages = "235--282" ) @article{randy02:fac , Author={R. Pollack} , Title={Dependently typed records in Type Theory} ,journal={Formal Aspects of Computing} , Year= 2002 , volume= {13} , pages={386--402}} @Article{PSS05:toplas, author = "F. Pottier and C. Skalka and S. Smith", title = "A systematic approach to static access control", journal = toplas, volume = "27", number = "2", pages = "344--382", month = mar, year = "2005", } @Article{PS03:toplas, author = "F. Pottier and V. Simonet", title = "Information flow inference for {ML}", journal = toplas, volume = "25", number = "1", pages = "117--158", month = jan, year = "2003" } @Article{plo75:tcs, title={Call-by-Name, Call-by-Value and the {$\lambda$}-Calculus}, author={G. Plotkin}, pages={125--159}, journal=tcs, year=1975, month=dec, volume=1, number=2 } @article (plo77:tcs, author = "G.D. Plotkin", title = "{LCF} Considered as a Programming Language", journal = tcs, year = 1977, volume = 5, pages = "223--255") @article{erik98:jfp, author={E. Poll}, title={Theoretical Pearl: Expansion Postponement for Normalizing Pure Type Systems}, year={1998}, journal=jfp, volume={8}, number={10}, pages={89--96}, month=jan} @article{pot77:aml, author={G. Pottinger}, title={Normalization as a homomorphic image of cut-elimination}, journal=aml, volume={12}, pages={323--357}, year={1977}} @article{PS:tcs, author={G. Pottinger and J. Seldin}, title={{Interpreting Church-style typed $\lambda$-calculus in Curry-style type assignment}}, journal=tcs, year={xxxx}, note={To appear}} @Article{reh96:ipl, title={Strong normalization for non-structural subtyping via saturated sets}, author={J. Rehof}, pages={157--162}, journal=ipl, month={27}, year=1996, volume=58, number=4} @Article{Reynolds98:hosc, author = "John C. Reynolds", title = "Definitional Interpreters for Higher-Order Programming Languages", journal = "Higher-Order and Symbolic Computation", year = 1998, volume = 11, number = 4, OPTpages = "7-105", note = "Reprinted from the proceedings of the 25th {ACM} National Conference (1972)" } @Article{rit91:jfp, author = "M. Rittri", title = "Using Types as Search Keys in Function Libraries", journal = jfp, volume = "1", number = "1", pages = "71--89", year = "1991"} @Article{RH03:jfp, author = {C. R\"ockl and D. Hirschkoff}, title = {A Fully Adequate Shallow Embedding of the $\pi$-Calculus in {Isabelle/HOL} with Mechanized Syntax Analysis}, journal = {Journal of Functional Programming}, year = 2003, volume=13, issue=2, pages={415-451}} @Article{san98:ic, title={An Interpretation of Typed Objects into Typed {$\pi$}-Calculus}, author={D. Sangiorgi}, pages={34--73}, journal=ic, month=may, year=1998, volume=143, number=1 } @Article{schn00:iss, author = "F. B. Schneider", title = "Enforceable Security Policies", journal = "ACM Transactions on Information and System Security", volume = "3", year = "2000", pages = "30--50", number = "1", month = feb} @Article{sel86:jsl, author = {Seldin, J.P.}, title = {On the Proof theory of the Intermediate Logic {MH}}, journal = jsl, year = 1986, volume = 51, number = 3, pages = {626--647} } @Article{sel89:sl, author = {Seldin, J.P.}, title = {Normalization and Excluded Middle}, journal = sl, year = 1989, volume = {XLVIII}, number = 2, pages = {193--217} } @Article{sel97:apal, title={On the proof theory of {Coquand's} calculus of constructions}, author={J.P. Seldin}, pages={23--101}, journal=apal, month=jan, year=1997, volume=83, number=1} @article(paula98:ic, author="Severi, P.", title={{Type Inference for Pure Type Systems}}, journal=ic, pages={1--23}, month=may, year=1998, volume=143, number=1) @Article{LS02:apal, author = "S. Soloviev and Z. Luo", title = "Coercion Completion and Conservativity in Coercive Subtyping", journal = apal, volume = "113", number = "1--3", pages = "297--322", year = "2002"} @Article{SA99:toplas, author = "R. Stata and M. Abadi", title = "A Type System for {Java} Bytecode Subroutines", journal = toplas, volume = "21", number = "1", pages = "90--137", month = jan, year = "1999"} @article{sta83:grund, author={R. Statman}, title={$\lambda$-definable functionals and $\beta\eta$-conversion}, year={1983}, journal=grund, pages={21--26}, volume={23} } @article{SS01:hosc, author = {A.~Sabelfeld and D.~Sands}, title = {A Per Model of Secure Information Flow in Sequential Programs}, journal = hosc, volume = {14}, number = {1}, year = {2001}, pages = {59--91} } @article{SM03:jsac, author={A. Sabelfeld and A. Myers}, title={{Language-Based Information-Flow Security}}, journal={{IEEE Journal on Selected Areas in Comunications}}, volume=21, issue=1, year=2003, month=jan, pages={5--19}} @Article{siv04:jlap, author = "I. A. Siveroni", title = "Operational semantics of the {Java Card Virtual Machine}", journal = "Journal of Logic and Algebraic Programming", volume = "58", number = "1--2", pages = "3--25", year = "2004" } @Article{str01:jsc, author = "S. Stratulat", title = "A General Framework to Build Contextual Cover Set Induction Provers", journal = jsc, volume = "32", number = "4", pages = "403--445", day = "1", month = sep, year = "2001"} @Article{thomas91:mscs, title={Dependence and independence results for (impredicative) calculi of dependent types}, author={T. Streicher}, pages={29--54}, journal=mscs, month=mar, year=1992, volume=2, number=1 } @Article{thomas92:tcs, title={Independence of the induction principle and the axiom of choice in the pure calculus of constructions}, author={T. Streicher}, pages={395--408}, journal=tcs, year=1992, month= sep, volume=103, number=2} @Article{TP00:acm, author = "F. Tip and J. Palsberg", title = "Scalable propagation-based call graph construction algorithms", journal = "ACM SIG{\-}PLAN Notices", volume = "35", number = "10", pages = "281--293", year = "2000"} @article{toy87:acm, author={Y. Toyama}, title={On the {Church-Rosser} Property for the Direct Sum of Term Rewriting Systems}, year={1987}, volume={34}, number={1}, pages={128-143}, journal=jacm} @Article{toy87:ipl, title={Counterexamples to termination for the direct sum of term rewriting systems}, author={Y. Toyama}, pages={141--143}, journal=ipl, year=1987, month= may, volume=25, number=3} @article{VS99:jcs, title={Probabilistic Noninterference in a Concurrent Language}, author={D. Volpano and G. Smith}, journal=jcs, volume=7, issue={2/3}, pages={231-253}, year=1999, month=nov} @Article{VSI96:jcs, title={{A Sound Type System for Secure Flow Analysis}}, author={D. Volpano and G. Smith and C. Irvine}, journal=jcs, voulem=4, issue=3, pages={167--187}, month=dec, year=1996} @Article{xi02:hosc, author = "H. Xi", title = "Dependent Types for Program Termination Verification", journal = "Higher-Order and Symbolic Computation", volume = "15", number = "1", pages = "91--131", month = mar, year = "2002", } @Article{zan94:jsc, author={H. Zantema}, title={Termination of Term Rewriting: Interpretation and Type Elimination}, journal=jsc, year=1994, volume=17, number=1, pages={23--50}, month=jan, keywords={Special Issue on Conditional Term Rewriting Systems} } @Article{ZM02:hosc, author = "S. Zdancewic and A.C. Myers", title = "Secure Information Flow via Linear Continuations", journal = "Higher-Order and Symbolic Computation", volume = "15", number = "2--3", pages = "209--234", month = sep, year = "2002"} @article{zuc74:aml, author={J. Zucker}, title={The correspondence between cut-elimination and normalization}, journal=aml, volume={7}, pages={113-155}, year={1974}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%% STOPPED HERE %%%%%%%%%%%%%%%% @misc{DGT98:sope, title = "Symposium on Partial Evaluation", year = "1998", author= "O. Danvy and R. Gl{\"u}ck and P. Thiemann, editors", journal=acmcs} @inproceedings{bie96:ll, author="G.M. Bierman", title="Towards a Classical Linear $\lambda$-calculus", booktitle="Proceedings of Tokyo Conference on Linear Logic", volume=3, series=entcs, publisher="Elsevier", year=1996 } @article{wan87:fi, author={M. Wand}, title={A simple algorithm and proof for type inference}, year={1987}, pages={115-122}, volume={X}, journal=FI} @Article{kri94:tcs, title={A general storage theorem for integers in call-by-name {$\lambda$}-calculus}, author={J.-L. Krivine}, journal=tcs, pages={79--94}, month=jun, year=1994, volume=129, number=1} @Article{reg94:tcs, title={Une {\'e}quivalence sur les lambda-termes}, author={L. Regnier}, journal=tcs, pages={281--292}, year=1994, volume=126, number=2} @Article{TF92:apal, title={On the adequacy of representing higher order intuitionistic logic as a pure type system}, author={H. Tonino and K. Fujita}, pages={251--276}, journal=apal, month=jun, year=1992, volume=57, number=3} @Article{sta91:jsl, title={Normalization Theorems for Full First Order Classical Natural Deduction}, author={G. St{\aa}lmarck}, pages={129--149}, journal=jsl, year=1991, month=mar, volume=56, number=1} @Article{nak94:apal, title={A constructive logic behind the catch and throw mechanism}, author={H. Nakano}, pages={269--301}, journal=apal, month=oct, year=1994, volume=69, number={2--3}} @incollection{KKSV95:jsc, author={R. Kennaway and J.W. Klop and R. Sleep and F.J. de Vries}, title= {Comparing curried and uncurried rewriting}, journal=jsc, year={1996}, note={To appear}} @Article{KOR93:tcs, author = "Klop, J.W. and Oostrom, V. van and Raamsdonk, F. van", title = "Combinatory Reduction Systems: Introduction and Survey", journal = tcs, volume = "121", number={1-2}, pages={279-308}, year = "1993"} @article (PT94:jfp, author = "B. Pierce and D. Turner" , title = "Simple Type-Theoretic Foundations for Object-Oriented Programming", journal = jfp, volume = 4, number = 2, pages = "207--247", year = "1994" ) @article{mul92:ipl, author={F. M{\"u}ller}, title={Confluence of the lambda calculus with left-linear algebraic rewriting}, journal=ipl, year={1992}, pages={293-299}, volume={41}} @article{yu , author={Y. Yu} , title={Computer proofs in group theory} , journal=jar , year=1990 , pages={251-286} , volume={6} , number={3} , month={September} } @article{imps, author={W. Farmer and J. Guttman and F. Thayer}, title={{\sc imps}: {an Interactive Mathematical Proof System}}, journal=jar, year={1993}, pages={231-248}, volume={11}} @article{telescope, author={N.G. de Bruijn}, title={Telescopic mappings in typed lambda calculus}, journal=ic, year={1991}, pages={189-204}, volume={91}, month={April}} @article{BTG:sn, author={V. Breazu-Tannen and J. Gallier}, title={Polymorphic rewriting conserves algebraic strong normalisation}, journal=tcs, volume={83}, pages={3-28}, year={1990}} @Article{FFKD87:tcs, title={A Syntactic Theory of Sequential Control}, author={M. Felleisen and D.P. Friedman and E. Kohlbecker and B.F. Duba}, pages={205--237}, journal=tcs, year=1987, volume=52, number=3} @article{morten97:ic, author = {S{\o}rensen, M.H.}, title = {Strong Normalization from Weak Normalization in Typed $\lambda$-Calculi}, pages={35--71}, month=feb, year=1997, volume=133, number=1, journal=ic } @Article{ter95:apal, title={Strong normalization in type systems: a model theoretic approach}, author={J. Terlouw}, pages={53--78}, journal=apal, month= may, year=1995, volume=73, number=1} @Article{the01:jar, author = "L. Th{\'e}ry", title = "A Certified Version of {Buchberger}'s Algorithm", journal = jar, volume = 26, issue=2, pages = {107-137}, year = 2001} @ARTICLE{haskell92, AUTHOR = {Hudak, P. and Peyton Jones, S.L. and Wadler, P.L. and Arvind and Boutel, B. and Fairbairn, J. and Fasel, J. and Guzman, K. and Hammond, K. and Hughes, J. and Johnsson, T. and Kieburtz, R. and Nikhil, R.S. and Partain, W. and Peterson, J.}, TITLE = {Report on the functional programming language {Haskell}, version 1.2}, JOURNAL = {Special Issue of SIGPLAN Notices}, VOLUME = {27}, YEAR = {1992} } @article{jon:jfp95, author={M. Jones}, title={A system of constructor classes: overloading and implicit higher-order polymorphism}, journal=jfp, pages={1-25}, month={January}, year={1995}} @article{rus87:ipl, author={M. Rusinowitch}, title={On termination of the direct sum of term-rewriting systems}, journal=ipl, pages={65-70}, volume={26}, year={1987}} @Article{DF92:mscs, title={Representing control: a study of the {CPS} transformation}, author={O. Danvy and A. Filinski}, pages={361--391}, journal=mscs, month=dec, year=1992, volume=2, number=4 } @Article{dan94:scp, title={Back to direct style}, author={O. Danvy}, pages={183--195}, journal=scp, month=jun, year=1994, volume=22, number=3 } @article{smi95:ijfcs, author={S. F. Smith}, title={Hybrid Partial-Total Type Theory}, journal={International Journal of Foundations of Computer Science}, volume=6, pages={235--263}, year={1995}} @Article{SAI98:popl, author = "A. Sa{\"\i}bi", title = "Typing Algorithm in Type Theory with Inheritance", journal = popl, volume = "24", year = "1997"} @article{DBLP:journals/tcs/DowekJ06, author = {Gilles Dowek and Ying Jiang}, title = {Eigenvariables, bracketing and the decidability of positive minimal predicate logic.}, journal = {Theor. Comput. Sci.}, volume = {360}, number = {1-3}, year = {2006}, pages = {193-208}, ee = {http://dx.doi.org/10.1016/j.tcs.2006.01.053}, bibsource = {DBLP, http://dblp.uni-trier.de} } @ARTICLE{Ghe:divftc, AUTHOR = "Giorgio Ghelli", TITLE = "Divergence of {$F_\leq$} Type Checking", JOURNAL = tcs, VOLUME = 139, NUMBER = "1--2", PAGES = "131--162", YEAR = 1995 }