@article{lmcs09,
  abstract = "Safety is a syntactic condition of higher-order grammars that constrains occurrences of variables in the production rules according to their type-theoretic order. In this paper, we introduce the safe lambda calculus, which is obtained by transposing (and generalizing) the safety condition to the setting of the simply-typed lambda calculus. In contrast to the original definition of safety, our calculus does not constrain types (to be homogeneous). We show that in the safe lambda calculus, there is no need to rename bound variables when performing substitution, as variable capture is guaranteed not to happen. We also propose an adequate notion of beta-reduction that preserves safety. In the same vein as Schwichtenberg's 1976 characterization of the simply-typed lambda calculus, we show that the numeric functions representable in the safe lambda calculus are exactly the multivariate polynomials; thus conditional is not definable. We also give a characterization of representable word functions. We then study the complexity of deciding beta-eta equality of two safe simply-typed terms and show that this problem is PSPACE-hard. Finally we give a game-semantic analysis of safety: We show that safe terms are denoted by `P-incrementally justified strategies'. Consequently pointers in the game semantics of safe lambda-terms are only necessary from order 4 onwards.",
  affiliation = "Univesity of Oxford",
  author = "William Blum and C.-H. Luke Ong",
  doi = "10.2168/LMCS-5(1:3)2009",
  journal = "Logic Methods in Computer Science",
  number = "1",
  publisher = "LMCS",
  title = "The Safe Lambda Calculus",
  url = "http://www.lmcs-online.org/ojs/viewarticle.php?id=424&layout=abstract",
  volume = "5",
  year = "2009",
}


    
      @inproceedings{HagueOng2007,
  author = "M. Hague and C.-H. L. Ong",
  booktitle = "FoSSaCS",
  note = "<a href="http://web.comlab.ox.ac.uk/people/Matthew.Hague/FoSSaCS07-long.pdf">Long Version (pdf)</a>",
  title = "Symbolic Backwards Reachability Analysis for Higher-Order Pushdown Systems",
  year = "2007",
}


    
      @techreport{RR-04-23,
  abstract = "Recent work by Knapik, Niwinski and Urzczyn [KNU02] has revived interest in the connexions between higher-order grammars and higher-order pushdown automata. Both devices can be viewed as definitions for term trees as well as string languages. In the latter setting we recall the extensive study by Damm [Dam82], and Damm and Goerdt [DG86]. There it was shown that the language of a level-<em>n</em>&nbsp;higher-order grammar is accepted by a level-<em>n</em>&nbsp;higher-order pushdown automaton subject to the restriction of&nbsp;<em>derived types,&nbsp;</em>more recent rebranded as&nbsp;<em>safety.</em>&nbsp;We show that at level 2, if a string language is generated by an unsafe grammar, there is a (level-2, non-deterministic) safe grammar that generates the same language. Thus safety is not a restriction for level-2 string languages.",
  author = "K. Aehlig and J. G. de Miranda and C.-H. L. Ong",
  institution = "Oxford University Computing Laboratory",
  month = "October",
  number = "RR-04-23",
  title = "Safety is not a restriction at level 2 for string languages",
  year = "2004",
}