Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
The Homepage of Tobias Gedell
Program languages: program analysis, type systems, semantics, implementation, functional programming
Program verification: interactive theorem proving, formal proofs
Security: information flow, non-interference, language-based verification
Publications
Abstract Interpretation Plugins for Type Systems
Tobias Gedell, Daniel Hedin
12th International Conference on Algebraic Methodology and Software Technology (AMAST'08)
(To appear.)
Verification by Parallelization of Parametric Code
Tobias Gedell, Reiner Hähnle
Algebraic and Proof-theoretic Aspects of Non-classical Logics Essays in honour of Professor Daniele Mundici on occasion of his 60th birthday
Springer-Verlag, LNCS 4460, 2007.
(Postscript - PDF - Abstract)
Polymorphism, Subtyping, Whole Program Analysis and Accurate Data Types in Usage Analysis
Tobias Gedell, Jörgen Gustavsson, Josef Svenningsson
The Fourth ASIAN Symposium on
Programming Languages and Systems (APLAS'06)
Springer-Verlag, LNCS 4279, 2006.
(Postscript - PDF - BibTeX - Abstract)
Automating Verification of Loops by Parallelization
Tobias Gedell, Reiner Hähnle
13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'06)
Springer-Verlag, LNCS 4246, 2006.
(Postscript - PDF - BibTeX - Abstract)
Static Analysis and Deductive Verification of Programs
Tobias Gedell
Licentiate thesis
Chalmers University of Technology, 2006.
(Postscript - PDF - BibTeX - Abstract)
Embedding Static Analysis into Tableaux and Sequent based Frameworks
Tobias Gedell
14th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'05)
Springer-Verlag, LNCS 3702, 2005.
(PDF - BibTeX - Abstract)
A Case Study on the Scalability of a Constraint Solving Algorithm: Polymorphic Usage Analysis with Subtyping
Tobias Gedell
Master's thesis
(Postscript - BibTeX - Abstract)
Drafts
Plugins for Structural Weakening and Strong Updates
Tobias Gedell, Daniel Hedin
Developed Software
Fire - A laboration submission and administration system.
CoreSA - Implementation of the usage analysis presented here in GHC.
SSC - A complete compiler for the STG language. Features type inference, garabage collection, unboxing, black holing, graph reduction and separate compilation.
CSHC - A Cache Sensitive Haskell Compiler which tries to generate cache optimized code.
ResNet - A distributed file system for UNIX with built-in redeandancy and load-balancing.