Bibliography

[2009] | [2008] | [2007] | [2006] | [2005] | [2004] | [2003] | [2002] | [2001] | [2000] | [1986]

2009

Domain Specific Languages (DSLs) for Network Protocols
Saleem Bhatti, Edwin Brady, Kevin Hammond, and James McKinna. Proc. International Workshop on Next Generation Network Architecture (NGNA 2009), Montreal, Canada, 2009. to appear
[BibTeX]
Correct-by-Construction Concurrency: using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols
Edwin Brady and Kevin Hammond. Fundamenta Informatica, 2009. to appear
[BibTeX]
Reasoning about Correctness Properties of a Coordination Language
Gudmund Grov. PhD Thesis. School of Mathematics and Computer Science, Heriot-Watt University, 2009.
[BibTeX]
Hume Cost Analyses for Imperative Programs
Gudmund Grov, Greg Michaelson, Christoph Herrmann, Hans-Wolfgang Loidl, Steffen Jost, and Kevin Hammond. Proc. 2009 International Conference on Software Engineering Theory and Practice (SETP 2009), 2009.
[BibTeX]
The Hume Report
K. Hammond and G. Michaelson. 2009 Version 0.3
[BibTeX] [PS]
Analysis Robustification
Jost, S. and Hammond, K. 2009 Deliverable D43
[BibTeX]
A Resource Logic for Hume
H-W. Loidl and L. Beringer. FM09 --- 16th International Symposium on Formal Methods, Eindhoven, The Netherlands, November 2--6, 2009. Submitted
[BibTeX]
Web site of the EmBounded Project (IST-510255)
Robert Rothenberg. 2009
[BibTeX] [URL]
Costing-by-construction Exemplar
Scaife, N; Loidl, H-W; Michaelson, G; and S'erot, J. 2009 Deliverable D44
[BibTeX]
Lazy Amortised Analysis?
Hugo Sim~oes. PhD Thesis. School of Computer Science, University of St Andrews, ?? 2009.
[BibTeX]

2008

A type system with usage aspects
David Aspinall, Martin Hofmann, and Michal Konecný. J. Funct. Program. 18 (2), 2008, pp. 141-178.
[BibTeX] [EE]
Lightweight Invariants with Full Dependent Types
Edwin Brady, Christoph Herrmann, and Kevin Hammond. Proc. International Symposium on Trends in Functional Programming (TFP 2008), 2008.
[BibTeX]
Nominal Renaming Sets
Murdoch James Gabbay and Martin Hofmann. LPAR, 2008, pp. 158-173.
[BibTeX] [EE]
Destructive Update and Dynamic Data Structures
Grov, G. and Michaelson, G. 2008 Deliverable D35
[BibTeX]
Preserving Coordination Properties when Transforming Concurrent System Components
Gudmund Grov, Robert Pointon, Greg Michaelson, and Andrew Ireland. Coordination Models, Languages and Applications Track of the 23rd Annual ACM Symposium on Applied Computing (SAC 2008), 2008.
[BibTeX] [URL]
Preserving Coordination Properties when Transforming Concurrent System Components
Gudmund Grov, Robert Pointon, Greg Michaelson, and Andrew Ireland. Coordination Models, Languages and Applications Track of the 23rd Annual ACM Symposium on Applied Computing, 2008.
[BibTeX] [PDF]
Finite Dimensional Vector Spaces Are Complete for Traced Symmetric Monoidal Categories
Masahito Hasegawa, Martin Hofmann, and Gordon D. Plotkin. Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, Arnon Avron, Nachum Dershowitz, and Alexander Rabinovich (eds.) , 2008, pp. 367-385.
[BibTeX] [URL]
Pure Pointer Programs with Iteration
Martin Hofmann and Ulrich Schöpp. CSL, 2008, pp. 79-93.
[BibTeX] [EE]
Validation of Space analyses
Jost, S. and Hammond, K. 2008 Deliverable D30
[BibTeX]
``Carbon Credits'' for Resource-Bounded Computations
Jost, S; Hammond, K; Loidl, H-W; and Hofmann, M. ICFP'08 --- Intl. Conference on Functional Programming, 2008. Submitted
[BibTeX]
A Semantic Proof of Polytime Soundness of Light Affine Logic
Ugo Dal Lago and Martin Hofmann. CSR, 2008, pp. 134-145.
[BibTeX] [EE]
Certificates
Loidl, H-W. and Beringer, L. 2008 Deliverable D21
[BibTeX]
Hume to HAM Translator
Pointon, R.F. and Scaife, N. 2008 Deliverable D23
[BibTeX]
Hume Machine Code Compiler
Pointon, R.F. and Scaife, N. 2008 Deliverable D24
[BibTeX]
Analyses Integrated into Compiler
Pointon, R.F; Scaife, N; and Loidl, H-W. 2008 Deliverable D25
[BibTeX]
Evaluation of Hume and the Hume Methodology
Scaife, N; Loidl, H-W; Michaelson, G; and Sérot, J. 2008 Deliverable D33
[BibTeX]
Real-time Computer Vision Algorithms
Sérot, J. and Scaife, N. 2008 Deliverable D27
[BibTeX]
Cost Inference and Analysis for Recursive Functional Programs
P.B. Vasconcelos. PhD Thesis. University of St Andrews, February 2008.
[BibTeX]
Space cost analysis using sized types
Pedro Baltazar Vasconcelos. PhD Thesis. School of Computer Science, University of St Andrews, November 2008.
[BibTeX] [URL]

2007

Automatic Amortised Worst-Case Execution Time Analysis
Christoph A.~Herrmann, Armelle Bonenfant, Kevin Hammond, Steffen Jost, Hans-Wolfgang Loidl, and Robert Pointon. 7th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis, Christine Rochange (ed.) , Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany, 2007.
[BibTeX] [URL]
Towards Resource-Certified Software: A Formal Cost Model for Time and its Application to an Image-Processing Example
Armelle Bonenfant, Zezhi Chen, Kevin Hammond, Greg Michaelson, Andy Wallace, and Iain Wallace. ACM Symposium on Applied Computing (SAC '07), Seoul, Korea, March 11-15, Seoul, Korea, 2007.
[BibTeX] [PDF] [URL]
Towards Resource-Certified Software: A Formal Cost Model for Time and its Application to an Image-Processing Example
Armelle Bonenfant, Zenzhi Chen, Kevin Hammond, Greg Michaelson, Andy Wallace, and Iain Wallace. ACM Symposium on Applied Computing (SAC '07), Seoul, Korea, March 11-15, 2007.
[BibTeX] [URL]
Worst-Case Execution Times for a Purely Functional Language
A. Bonenfant, C. Ferdinand, K. Hammond, and R. Heckmann. Proc. 2006 Intl. Symp. on Impl. and Appl. of Functional Langs. (IFL 2006), Springer-Verlag LNCS 4449, 2007, pp. 235--252.
[BibTeX]
Automatic Amortised Worst-Case Execution Time Analysis
C.~Herrmann, A.~Bonenfant, K.~Hammond, S.~Jost, H.-W.~Loidl, and R.~Pointon. 7th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis, 2007.
[BibTeX]
Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types
Edwin Brady, James McKinna, and Kevin Hammond. Proc. International Symposium on Trends in Functional Programming (TFP 2007), 2007.
[BibTeX]
Static Memory and Timing Analysis of Embedded Systems Code
Christian Ferdinand, Reinhold Heckmann, and Bärbel Franzen. Proceedings of VVSS2007 - 3rd European Symposium on Verification and Validation of Software Systems, 23rd of March 2007, Eindhoven, Perry Groot (ed.) , 2007.
[BibTeX] [URL]
Using Mean-Shift Tracking Algorithms for Real-Time Tracking of Moving Images on an Autonomous Vehicle Testbed Platform
Benjamin Gorry, Zezhi Chen, Kevin Hammond, Andy Wallace, and Greg Michaelson. IRMA 2007, International Conference on Intelligent Robotics and Manufacturing Automation, Venice, Italy, November 23-25, 2007, 2007, 25, World Academy of Science, Engineering and Technology (PWASET), 2007.
[BibTeX] [URL]
Compiler Support Tools
Grov, G. 2007 Deliverable D26
[BibTeX]
Towards a Box Calculus for Hierarchical Hume
Gudmond Grov and Greg Michaelson. Trends in Functional Programming, Marco T. Morazan (ed.) : 8, Intellect, 2007.
[BibTeX] [URL]
Formal Verification of Concurrent Scheduling Strategies using TLA
Gudmund Grov, Greg Michaelson, and Andrew Ireland. 3rd IEEE International Workshop on Scheduling and Resource Management for Parallel and Distributed Systems, IEEE, 2007.
[BibTeX] [URL]
Fourth Project Workshop
Hammond, K. 2007 Deliverable D19
[BibTeX]
Low-Level Programming in Hume: an Exploration of the HW-Hume Level
Kevin Hammond, Gudmund Grov, Greg Michaelson, and Andrew Ireland. Proc. Implementation of Functional Languages (IFL 2006), Springer-Verlag LNCS 4449, 2007, pp. 91--107.
[BibTeX]
Automatic Amortised Worst-Case Execution Time Analysis
Christoph A. Herrmann, Armelle Bonenfant, Kevin Hammond, Steffen Jost, Hans-Wolfgang Loidl, and Robert Pointon. 7th Int'l Workshop on Worst-Case Execution Time (WCET) Analysis, Proceedings, Pisa, Italy, July 3, 2007, 2007, pp. 13--18.
[BibTeX] [PDF] [URL]
Prototype Implementation of Space Analyses
Jost, S. 2007 Deliverable D13
[BibTeX]
Prototype Implementation of Time Analysis
Jost, S. 2007 Deliverable D15
[BibTeX]
Validation of the Prototype Worst-Case Executation Time (WCET) analysis
Jost, S. and Hammond, K. 2007 Deliverable D16
[BibTeX]
Report on Stack-space Analysis
Jost, S; Loidl, H-W; and Hammond, K. 2007 Deliverable D5
[BibTeX]
Report on Heap-space Analysis
Jost, S; Loidl, H-W; and Hammond, K. 2007 Deliverable D11
[BibTeX]
Report on WCET Analysis
Jost, S; Loidl, H-W; and Hammond, K. 2007 Deliverable D14
[BibTeX]
HW-Hume in Isabelle
Chunxu Liu and Greg Michaelson. Draft Proceedings of 19th International Symposium on Implementation and Application of Functional Languages, O. Chitil (ed.) , Computing Laboratory, University of Kent, 2007.
[BibTeX] [URL]
Assertion Language
Loidl, H-W. and Grov, G. 2007 Deliverable D17
[BibTeX]
Mobile Resource Guarantees (project evaluation paper)
D. Sannella, M. Hofmann, D. Aspinall, S. Gilmore, I. Stark, L. Beringer, H-W. Loidl, K. MacKenzie, A. Momigliano, and O. Shkaravska. TFP05: Trends in Functional Programing, Intellect, Tallinn, Estonia, 2007, pp. 211--226.
[BibTeX] [URL]
Intersection Types for Cost-analysis of Functional Programs
Hugo R. Simoes, Kevin Hammond, M'ario Florido, and Pedro Vasconcelos. Proc. 2006 International Conf. on Types (TYPES 2006), Springer-Verlag LNCS, 2007.
[BibTeX]
The Worst-Case Execution Time Problem --- Overview of Methods and Survey of Tools
Reinhard Wilhelm, Jakob Engblom, Andreas Ermedahl, Niklas Holsti, Stephan Thesing, David Whalley, Guillem Bernat, Christian Ferdinand, Reinhold Heckmann, Tulika Mitra, Frank Mueller, Isabelle Puaut, Peter Puschner, Jan Staschulat, and Per Stenström. ACM Transactions on Embedded Computing Systems, 2007. To appear
[BibTeX]

2006

Reading, Writing and Relations
N. Benton, A. Kennedy, M. Hofmann, and L. Beringer. Proc. Fourth ASIAN Symposium on Programming Languages and Systems (APLAS 2006), Sydney, Australia, 2006.
[BibTeX]
A Bytecode Logic for JML and Types
L. Beringer and M. Hofmann. Proc. Fourth ASIAN Symposium on Programming Languages and Systems (APLAS 2006), Sydney, Australia, 2006.
[BibTeX]
A Dependently Typed Framework for Static Analysis of Program Execution Costs
Edwin Brady and Kevin Hammond. Implementation of Functional Languages (IFL) 2005, Lecture Notes in Computer Science 4015, Springer, Berlin/Heidelberg, 2006, pp. 74-90.
[BibTeX] [DOI] [PDF]
A Verified Staged Interpreter is a Verified Compiler: Multi-stage Programming with Dependent Types
Edwin Brady and Kevin Hammond. Proc. Conf. Generative Programming and Component Engineering (GPCE '06), Portland, Oregon, Lecture Notes in Computer Science, Springer, 2006.
[BibTeX] [PDF]
A Proof System for the Linear Time <span class='mathrm'>μ</span>-Calculus
C. Dax, M. Hofmann, and M. Lange. Proc. Conf. on Foundations of Software Technology and Theoretical Computer Science, Kolkata, India, 2006.
[BibTeX]
EmBounded: Formally Embedded Systems
The EmBounded Project. The House Magazine, Dods Parliamentary Communications, Ltd, November 2006. Advertisement.
[BibTeX] [PDF]
Improved Worst-Case Execution Time Prediction via Execution Contexts
Christian Ferdinand and Reinhold Heckmann. Proc. Embedded World 2006 Conference,N"urnberg, Germany, 2006.
[BibTeX]
Verifying Timing Properties of Safety-Critical Embedded Software by Abstract Interpretation
Christian Ferdinand and Reinhold Heckmann. Proc. Embedded Real Time Software Congress (ERTS 2006), Toulouse, France, 2006.
[BibTeX]
An Abstract Machine Implementation for Hume
K. Hammond. 2006
[BibTeX]
Exploiting Purely Functional Programming to Obtain Bounded Resource Behaviour: the Hume Approach
Kevin Hammond. First Central European Summer School, CEFP 2005, Budapest, Hungary, July 4-15, 2005, Revised Selected Lectures, Zoltán Horváth (ed.) : Lecture Notes in Computer Science 4164, Springer-Verlag, 2006, pp. 100-134.
[BibTeX] [DOI] [PDF] [ISBN]
The EmBounded project (project paper)
Kevin Hammond, Roy Dyckhoff, Christian Ferdinand, Reinhold Heckmann, Martin Hofmann, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Jocelyn Sérot, and Andy Wallace. Proc. 6th Symposium on Trends in Functional Programming (TFP 2005), Tallinn, Estonia, 23-24 September 2005, Trends in Functional Programming 6, Intellect, 2006.
[BibTeX] [PDF]
The EmBounded Project: Automatic Prediction of Resource Bounds for Embedded Systems
Kevin Hammond, Roy Dyckhoff, Christian Ferdinand, Reinhold Heckmann, Martin Hofmann, Hans-Wolfgang Loidl, Greg Michaelson, Jocelyn S'erot, and Andy Wallace. Trends in Functional Programming, Volume 6, 2006.
[BibTeX]
Towards Formally Verifiable Resource Bounds for Real-Time Embedded Systems
Kevin Hammond, Christian Ferdinand, Reinhold Heckmann, Roy Dyckhoff, Martin Hoffmann, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Robert Pointon, Norman Scaife, Jocelyn Sérot, and Andy Wallace. Proc. Workshop on Innovative Techniques for Certification of Embedded Systems, 2006.
[BibTeX] [PDF]
Towards Formally Verifiable WCET Analysis for a Functional Programming Language
Kevin Hammond, Christian Ferdinand, Reinhold Heckmann, Roy Dyckhoff, Martin Hofman, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Robert Pointon, Norman Scaife, Jocelyn Sérot, and Andy Wallace. 6th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis, Frank Mueller (ed.) : Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, Dagstuhl, Germany, 2006.
[BibTeX] [PDF] [URL]
Bounded Space Programming using Finite State Machines and Recursive Functions: the Hume Approach
Kevin Hammond, Greg Michaelson, and Pedro Vasconcelos. ACM Transactions on Software Engineering Methodology, 2006. Submitted
[BibTeX] [PDF]
Static Memory and Execution Time Analysis of Embedded Code
Reinhold Heckmann and Christian Ferdinand. Proc. SAE World Congress, Michigan, USA, 2006.
[BibTeX]
Type-based Amortised Heap-Space Analysis (for an Object-Oriented Language)
Hofmann, Martin and Jost, Steffen. Proceedings of the 15th European Symposium on Programming (ESOP), Peter Sestoft (ed.) : Lecture Notes in Computer Science (LNCS) 3924, Springer-Verlag, 2006.
[BibTeX] [URL]
Type-based Amortised Heap-Space Analysis (for an Object-Oriented Language)
Hofmann, Martin and Jost, Steffen. Proceedings of the 15th European Symposium on Programming (ESOP), Peter Sestoft (ed.) : Lecture Notes in Computer Science (LNCS) 3924, Springer-Verlag, 2006.
[BibTeX] [URL]
Type-Based Amortised Heap-Space Analysis.
Martin Hofmann and Steffen Jost. Programming Languages and Systems : 15th European Symposium on Programming, ESOP 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 27-28, 2006, Peter Sestoft (ed.) : Lecture Notes in Computer Science 3924, Springer-Verlag, 2006, pp. 22-37.
[BibTeX] [DOI] [ISBN]
Well-foundedness in Realizability
M. Hofmann, J. van Oosten, and T. Streicher. Archive for Mathematical Logic 45 (7), 2006, pp. 795--805.
[BibTeX]
Automated WCET Analysis based on Program Modes
Meng-Luo Ji, Ji Wang, Shuhao Li, and Zhi-Chang Qi. AST'06, ACM Press, 2006, pp. 36-42.
[BibTeX]
Formal Hume Semantics
Jost, S. 2006 Deliverable D12
[BibTeX]
Cost Model
Loidl, H-W. and Hammond, K. 2006 Deliverable D4
[BibTeX]
Recursion, Iteration and Hume Scheduling
Greg Michaelson and Robert Pointon. Trends in Functional Programming (TFP'06), Nottingham UK, 2006.
[BibTeX]
Toward Resource Certified Image Processing Software
Greg Michaelson, Andy Wallace, Kevin Hammond, Iain Wallace, Armelle Bonenfant, and Zezhi Chen. Systems Engineering for Autonomous Systems Defence Technology Centre (SEAS DTC), Annual Technical Conference, July 2006, Edinburgh, Conference Proceedings, Edinburgh, UK MoD, 2006, pp. A15.
[BibTeX] [PDF] [URL]
Compiling vs Costing - Experiences With Hume
Robert F. Pointon. Implementation of Functional Languages (IFL'06), Budapest Hungary, 2006.
[BibTeX]
Real-time Testbed Applications
Jocelyn Serot and Norman Scaife. 2006 Laboratoire LASMEA, Blaise Pascal University
[BibTeX]
Real-time Testbed Applications
Jocelyn Serot and Norman Scaife. 2006 Deliverable D7
[BibTeX]

2005

Mobile Resource Guarantees for Smart Devices
David Aspinall, Stephen Gilmore, Martin Hofmann, Donald Sannella, and Ian Stark. Construction and Analysis of Safe, Secure, and Interoperable Smart Devices: Proceedings of the International Workshop CASSIS 2004, Marseille, LNCS 3362, Springer, 2005, pp. 1--26.
[BibTeX] [PDF] [URL]
Automatic Certification of Heap Consumption
Beringer, L; Hofmann, M; Momigliano, A; and Shkaravska, O. LPAR 2004 --- Logic for Programming, Artificial Intelligence, and Reasoning, Franz Baader, Andrei Voronkov (ed.) : LNCS 3452, Springer, Montevideo, Uruguay, March 14--18, 2005, pp. 347--362.
[BibTeX] [PDF]
Exploiting Purely Functional Programming to Obtain Bounded Resource Behaviour: The Hume Approach
Kevin Hammond. CEFP, 2005, pp. 100-134.
[BibTeX] [EE]
Is it Time for Real-Time Functional Programming?
Kevin Hammond. Trends in Functional Programming, Volume 4, Stephen Gilmore (ed.) : Trends in Functional Programming 4, Intellect, 2005, pp. 1-14.
[BibTeX] [ISBN]
The EmBounded project (project paper)
Kevin Hammond, Roy Dyckhoff, Christian Ferdinand, Reinhold Heckmann, Martin Hofmann, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Jocelyn Sérot, and Andy Wallace. Proc. 6th Symposium on Trends in Functional Programming (TFP 2005), Tallinn, Estonia, 23-24 September 2005, Institute of Cybernetics, 2005, pp. 220-235. Online
[BibTeX] [URL]
Certification of Quantitative Properties of Programs
M. Hofmann, H-W. Loidl, and L. Beringer, IOS Press, 2005. Marktoberdorf Summer School, Aug 2-13, 2005
[BibTeX] [URL]
FSM-Hume is Finite State
Greg Michaelson, Kevin Hammond, and Jocelyn Sérot. Trends in Functional Programming, Volume 4, Stephen Gilmore (ed.) : Trends in Functional Programming 4, Intellect, 2005, pp. 19-28.
[BibTeX] [ISBN]

2004

Model Checking HW-Hume
G. Grov. Master's Thesis. Heriot-Watt University, 2004.
[BibTeX]

2003

An Abstract Machine for Resource Bounded Computations in Hume
Hammond, K. IFL03 --- Intl Workshop on Implementation of Functional Languages, Edinburgh, Scotland, 2003, pp. 79--94. Draft proceedings
[BibTeX]
Static Prediction of Heap Space Usage for First-Order Functional Programs
Hofmann, Martin and Jost, Steffen. Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2003, pp. 185--197.
[BibTeX] [URL]

2002

Another Type System for In-Place Update
Aspinall, D. and Hofmann, M. ESOP'02 --- European Symposium on Programming, LNCS~2305, Springer-Verlag, 2002, pp. 36--52.
[BibTeX] [URL]
Predictable Space Behaviour in FSM-Hume
K. Hammond and G.J. Michaelson. 14th Intl Workshop on Implementation of Functional Languages, Madrid, Spain, 2002, pp. 386--403.
[BibTeX]
Cost Analysis using Automatic Size and Time Inference
A.J. Reb'on Portillo, K. Hammond, and H.-W. Loidl. 14th Intl Workshop on Implementation of Functional Languages, Madrid, Spain, 2002, pp. 1--13.
[BibTeX]

2001

Mobile Resource Guarantees
2001 EU Project No. IST-2001-33149, for further information see http://www.dcs.ed.ac.uk/home/mrg/
[BibTeX]

2000

A type system for bounded space and functional in-place update
M. Hofmann. Nordic Journal of Computing 7 (4), 2000, pp. 258--289.
[BibTeX] [URL]

1986

Interpreters from functions and grammars
G. Michaelson. Computer Languages 11 (2), 1986, pp. 85-104.
[BibTeX]

This page was last modified on Sunday 3 May 2009 23:48:58. This site is maintained by Robert Rothenberg (r r at cs dot st - andrews dot ac dot uk).