Higher-Order and Symbolic Computation, Volume 20

Volume 20, Numbers 1-2, June 2007

• Narciso Martí-Oliet, Grigore Rosu, Carolyn L. Talcott:
  Editorial. 1-2
  
• Iliano Cervesato, Mark-Oliver Stehr:
  Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types. 3-35
  
• Horatiu Cirstea, Germain Faure, Claude Kirchner:
  A rho-calculus of explicit constraint application. 37-72
  
• Francisco Javier López-Fraguas, Mario Rodríguez-Artalejo, Rafael del Vado Vírseda:
  A new generic scheme for functional logic programming with constraints. 73-122
  
• José Meseguer, Prasanna Thati:
  Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. 123-160
  
• Peter Csaba Ölveczky, José Meseguer:
  Semantics and pragmatics of Real-Time Maude. 161-196
  

Volume 20, Number 3, September 2007

• Olivier Danvy:
  Editorial. 197-198
  
• Jean-Louis Krivine:
  A call-by-name lambda-calculus machine. 199-207
  
• Pierre Crégut:
  Strongly reducing variants of the Krivine abstract machine. 209-230
  
• Mitchell Wand:
  On the correctness of the Krivine machine. 231-235
  
• Rémi Douence, Pascal Fradet:
  The next 700 Krivine machines. 237-255
  
• Frédéric Lang:
  Explaining the lazy Krivine machine using explicit substitution and addresses. 257-270
  
• Daniel P. Friedman, Abdulaziz Ghuloum, Jeremy G. Siek, Onnie Lynn Winebarger:
  Improving the lazy Krivine machine. 271-293
  
• Sylvain Lippi:
  The graphical Krivine machine. 295-318
  
• David A. Schmidt:
  State-transition machines for lambda-calculus expressions. 319-332
  
• David A. Schmidt:
  State-transition machines, revisited. 333-335
  

Volume 20, Number 4, December 2007

• Olivier Danvy, Hayo Thielecke:
  Editorial. 337-338
  
• Yukiyoshi Kameyama:
  Axioms for control operators in the CPS hierarchy. 339-369
  
• Chung-chieh Shan:
  A static simulation of dynamic delimited control. 371-401
  
• Zena M. Ariola, Hugo Herbelin, Amr Sabry:
  A proof-theoretic foundation of abortive continuations. 403-429
  
• Shriram Krishnamurthi, Peter Walton Hopkins, Jay A. McCarthy, Paul T. Graunke, Greg Pettyjohn, Matthias Felleisen:
  Implementation and use of the PLT scheme Web server. 431-460