Martin Hofmann

Daniel Wagner

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013

Power of Nondetreministic JAGs on Cayley graphs.

[BibT_eX]

[DOI]

Ramyaa Ramyaa

CoRR, 2013

Verifying pointer and string analyses with region type systems.

[BibT_eX]

[DOI]

Robert Grabowski

Comput. Lang. Syst. Struct., 2013

Computing With a Fixed Number of Pointers (Invited Talk).

[BibT_eX]

[DOI]

Ramyaa

Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2013

Pure Pointer Programs and Tree Isomorphism.

[BibT_eX]

[DOI]

Ramyaa Ramyaa

Ulrich Schöpp

Proceedings of the Foundations of Software Science and Computation Structures, 2013

On Monadic Parametricity of Second-Order Functionals.

[BibT_eX]

[DOI]

Andrej Bauer

Aleksandr Karbyshev

Proceedings of the Foundations of Software Science and Computation Structures, 2013

Automatic Type Inference for Amortised Heap-Space Analysis.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2013

2012

Multivariate amortized resource analysis.

[BibT_eX]

[DOI]

Klaus Aehlig

ACM Trans. Program. Lang. Syst., 2012

Learn with SAT to Minimize Büchi Automata

[BibT_eX]

[DOI]

Stephan Barth

Proceedings of the Proceedings Third International Symposium on Games, 2012

Edit lenses.

[BibT_eX]

[DOI]

Daniel Wagner

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Linear Constraints over Infinite Trees.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Resource Aware ML.

[BibT_eX]

[DOI]

Klaus Aehlig

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011

Realizability models and implicit complexity.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2011

Symmetric lenses.

[BibT_eX]

[DOI]

Daniel Wagner

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Type-Based Enforcement of Secure Programming Guidelines - Code Injection Prevention at SAP.

[BibT_eX]

[DOI]

Robert Grabowski

Keqin Li

Proceedings of the Formal Aspects of Security and Trust - 8th International Workshop, 2011

Automatentheorie und Logik.

[BibT_eX]

[DOI]

Martin Lange

eXamen.press, Springer, ISBN: 978-3-642-18089-7, 2011

2010

Pure pointer programs with iteration.

[BibT_eX]

[DOI]

Ulrich Schöpp

ACM Trans. Comput. Log., 2010

A Semantic Proof of Polytime Soundness of Light Affine Logic.

[BibT_eX]

[DOI]

Theory Comput. Syst., 2010

Bounded Linear Logic, Revisited

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2010

Verifying a Local Generic Solver in Coq.

[BibT_eX]

[DOI]

Aleksandr Karbyshev

Helmut Seidl

Proceedings of the Static Analysis - 17th International Symposium, 2010

Type inference in intuitionistic linear logic.

[BibT_eX]

[DOI]

Patrick Baillot

Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2010

Static determination of quantitative resource usage for higher-order programs.

[BibT_eX]

[DOI]

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

What Is a Pure Functional?

[BibT_eX]

[DOI]

Aleksandr Karbyshev

Helmut Seidl

Proceedings of the Automata, Languages and Programming, 37th International Colloquium, 2010

Amortized Resource Analysis with Polynomial Potential.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2010

10351 Executive Summary - Modelling, Controlling and Reasoning About State.

[BibT_eX]

[DOI]

Proceedings of the Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010, 2010

10351 Abstracts Collection - Modelling, Controlling and Reasoning About State.

[BibT_eX]

[DOI]

Proceedings of the Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010, 2010

Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems - 8th Asian Symposium, 2010

2009

Relational semantics for effect-based program transformations: higher-order store.

[BibT_eX]

[DOI]

Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2009

"Carbon Credits" for Resource-Bounded Computations Using Amortised Analysis.

[BibT_eX]

[DOI]

Proceedings of the FM 2009: Formal Methods, 2009

Membership Checking in Greatest Fixpoints Revisited.

[BibT_eX]

[DOI]

Proceedings of the 6th Workshop on Fixed Points in Computer Science, 2009

Efficient Type-Checking for Amortised Heap-Space Analysis.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 23rd international Workshop, 2009

2008

A type system with usage aspects.

[BibT_eX]

[DOI]

David Aspinall

Michal Konecný

J. Funct. Program., 2008

Pointer Programs and Undirected Reachability.

[BibT_eX]

[DOI]

Ulrich Schöpp

Electron. Colloquium Comput. Complex., 2008

A Bytecode Logic for JML and Types.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2008

Secure information flow and program logics.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2008

Nominal Renaming Sets.

[BibT_eX]

[DOI]

Murdoch James Gabbay

Proceedings of the Logic for Programming, 2008

08061 Abstracts Collection -- Types, Logics and Semantics for State.

[BibT_eX]

[DOI]

Proceedings of the Types, Logics and Semantics for State, 03.02. - 08.02.2008, 2008

08061 Executive Summary -- Types, Logics and Semantics for State.

[BibT_eX]

[DOI]

Proceedings of the Types, Logics and Semantics for State, 03.02. - 08.02.2008, 2008

Finite Dimensional Vector Spaces Are Complete for Traced Symmetric Monoidal Categories.

[BibT_eX]

[DOI]

Masahito Hasegawa

Gordon D. Plotkin

Proceedings of the Pillars of Computer Science, 2008

2007

A program logic for resources.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2007

Elimination of Ghost Variables in Program Logics.

[BibT_eX]

[DOI]

Mariela Pavlova

Proceedings of the Trustworthy Global Computing, Third Symposium, 2007

Relational semantics for effect-based program transformations with dynamic allocation.

[BibT_eX]

[DOI]

Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2007

Certification Using the Mobius Base Logic.

[BibT_eX]

[DOI]

Mariela Pavlova

Proceedings of the Formal Methods for Components and Objects, 6th International Symposium, 2007

2006

Preface.

[BibT_eX]

[DOI]

Hans-Wolfgang Loidl

Theor. Comput. Sci., 2006

Consistency of the theory of contexts.

[BibT_eX]

[DOI]

J. Funct. Program., 2006

Well-foundedness in Realizability.

[BibT_eX]

[DOI]

Jaap van Oosten

Arch. Math. Log., 2006

Towards Formally Verifiable WCET Analysis for a Functional Programming Language.

[BibT_eX]

[DOI]

Proceedings of the 6th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis, 2006

MOBIUS: Mobility, Ubiquity, Security.

[BibT_eX]

[DOI]

Proceedings of the Trustworthy Global Computing, Second Symposium, 2006

A Proof System for the Linear Time µ-Calculus.

[BibT_eX]

[DOI]

Christian Dax

Martin Lange

Proceedings of the FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 2006

Type-Based Amortised Heap-Space Analysis.

[BibT_eX]

[DOI]

Steffen Jost

Proceedings of the Programming Languages and Systems, 2006

Reading, Writing and Relations.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 4th Asian Symposium, 2006

2005

Typed Lambda Calculi and Applications 2003, Selected Papers.

[BibT_eX]

[DOI]

Pawel Urzyczyn

Fundam. Informaticae, 2005

Mobile Resource Guarantees (project evaluation paper).

[BibT_eX]

Proceedings of the Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, 2005

The Embounded project (project start paper).

[BibT_eX]

Proceedings of the Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, 2005

Proof-Theoretic Approach to Description-Logic.

[BibT_eX]

[DOI]

Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 2005

Quantitative Models and Implicit Complexity.

[BibT_eX]

[DOI]

Proceedings of the FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 2005

2004

Realizability models for BLL-like languages.

[BibT_eX]

[DOI]

Philip J. Scott

Theor. Comput. Sci., 2004

An arithmetic for non-size-increasing polynomial-time computation.

[BibT_eX]

[DOI]

Klaus Aehlig

Ulrich Berger

Helmut Schwichtenberg

Theor. Comput. Sci., 2004

On the non-sequential nature of the interval-domain model of real-number computation.

[BibT_eX]

[DOI]

Martín Hötzel Escardó

Math. Struct. Comput. Sci., 2004

A Program Logic for Resource Verification.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

Automatic Certification of Heap Consumption.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2004

What Do Program Logics and Type Systems Have in Common?

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming: 31st International Colloquium, 2004

04381 Abstracts Collection - Dependently Typed Programming.

[BibT_eX]

[DOI]

Thorsten Altenkirch

John Hughes

Proceedings of the Dependently Typed Programming, 12.09. - 17.09.2004, 2004

Mobile Resource Guarantees for Smart Devices.

[BibT_eX]

[DOI]

Proceedings of the Construction and Analysis of Safe, 2004

2003

Preface.

[BibT_eX]

[DOI]

Jirí Adámek

Martín Hötzel Escardó

Theor. Comput. Sci., 2003

Linear types and non-size-increasing polynomial time computation.

[BibT_eX]

[DOI]

Inf. Comput., 2003

Static prediction of heap space usage for first-order functional programs.

[BibT_eX]

[DOI]

Steffen Jost

Proceedings of the Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2003

Certification of Memory Usage.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Computer Science, 8th Italian Conference, 2003

2002

A New "Feasible" Arithmetic.

[BibT_eX]

[DOI]

Stephen J. Bellantoni

J. Symb. Log., 2002

Completeness of Continuation Models for lambda-mu-Calculus.

[BibT_eX]

[DOI]

Inf. Comput., 2002

Type Destructors.

[BibT_eX]

[DOI]

Inf. Comput., 2002

The strength of non-size increasing computation.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002

Another Type System for In-Place Update.

[BibT_eX]

[DOI]

David Aspinall

Proceedings of the Programming Languages and Systems, 2002

2001

From Bounded Arithmetic to Memory Management: Use of Type Theory to Capture Complexity Classes and Space Behaviour.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 5th International Conference, 2001

The Strength of Non-size-increasing Computation (Introduction and Summary).

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 2001, 2001

Normalization by Evaluation for Typed Lambda Calculus with Coproducts.

[BibT_eX]

[DOI]

Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

2000

Programming languages capturing complexity classes.

[BibT_eX]

[DOI]

SIGACT News, 2000

A Type System for Bounded Space and Functional In-Place Update.

[BibT_eX]

Nord. J. Comput., 2000

Safe recursion with higher types and BCK-algebra.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2000

Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover.

[BibT_eX]

[DOI]

Francis Tang

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

A Type System for Bounded Space and Functional In-Place Update--Extended Abstract.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2000

1999

Preface.

[BibT_eX]

[DOI]

Giuseppe Rosolini

Dusko Pavlovic

Proceedings of the Conference on Category Theory and Computer Science, 1999

A new method for establishing conservativity of classical systems over their intuitionistic version.

[BibT_eX]

[DOI]

Thierry Coquand

Math. Struct. Comput. Sci., 1999

Semantics of Linear/Modal Lambda Calculus.

[BibT_eX]

[DOI]

J. Funct. Program., 1999

Semantical Analysis of Higher-Order Abstract Syntax.

[BibT_eX]

[DOI]

Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

1998

Inheritance of Proofs.

[BibT_eX]

Wolfgang Naraschewski

Martin Steffen

Terry Stroup

Theory Pract. Object Syst., 1998

1997

An application of category-theoretic semantics to the characterisation of complexity classes using higher-order function algebras.

[BibT_eX]

[DOI]

Bull. Symb. Log., 1997

Continuation Models are Universal for Lambda-Mu-Calculus.

[BibT_eX]

[DOI]

Proceedings of the Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29, 1997

A Mixed Modal/Linear Lambda Calculus with Applications to Bellantoni-Cook Safe Recursion.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 11th International Workshop, 1997

Extensional constructs in intensional type theory.

[BibT_eX]

CPHC/BCS distinguished dissertations, Springer, ISBN: 978-3-540-76121-1, 1997

1996

On Behavioural Abstraction and Behavioural Satisfaction in Higher-Order Logic.

[BibT_eX]

[DOI]

Donald Sannella

Theor. Comput. Sci., 1996

Positive Subtyping.

[BibT_eX]

[DOI]

Inf. Comput., 1996

Reduction-Free Normalisation for a Polymorphic System.

[BibT_eX]

Thorsten Altenkirch

Proceedings of the Fourth Israel Symposium on Theory of Computing and Systems, 1996

1995

Sound and Complete Axiomatisations of Call-by-Value Control Operators.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 1995

A Unifying Type-Theoretic Framework for Objects.

[BibT_eX]

[DOI]

J. Funct. Program., 1995

Conservativity of Equality Reflection over Intensional Type Theory.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, 1995

A Simple Model for Quotient Types.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 1995

On Behavioral Abstraction and Behavioural Satisfaction in Higher-Order Logic.

[BibT_eX]

[DOI]

Donald Sannella

Proceedings of the TAPSOFT'95: Theory and Practice of Software Development, 1995

Categorical Reconstruction of a Reduction Free Normalization Proof.

[BibT_eX]

[DOI]

Thorsten Altenkirch

Proceedings of the Category Theory and Computer Science, 6th International Conference, 1995

1994

The Groupoid Model Refutes Uniqueness of Identity Proofs

[BibT_eX]

[DOI]

Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

On the Interpretation of Type Theory in Locally Cartesian Closed Categories.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 8th International Workshop, 1994

1993

Elimination of Extensionality in Martin-Löf Type Theory.

[BibT_eX]

[DOI]