Jan Hoffmann, Aufgabensteller Prof, Dr. Martin Hofmann, Betreuer Prof, Samuel R. Buss, Ph. D
This thesis analyzes the connections between resolution proofs and satisfiability search procedures. It is well known that DLL search algorithms that do not use learning are equivalent to tree-like...
Pure Pointer Programs with Iteration (2009)
Abstract. Many LOGSPACE algorithms are naturally described as programs that operate on a structured input (e.g. a graph), that store in memory only a constant number of pointers (e.g. to graph nodes)...
Jan Hoffmann, Aufgabensteller Prof, Dr. Martin Hofmann, Betreuer Prof, Samuel R. Buss, Ph. D
This thesis analyzes the connections between resolution proofs and satisfiability search procedures. It is well known that DLL search algorithms that do not use learning are equivalent to tree-like...
Bounded Linear Logic, Revisited (2009)
Lago, Ugo Dal, Hofmann, Martin
We present QBAL, an extension of Girard, Scedrov and Scott's bounded linear logic. The main novelty of the system is the possibility of quantifying over resource variables. This generalization makes...
CitationBase: A social tagging management for references (2009)
Social tagging is one of the major phenomena brought by the social media and technologies in the Web2.0. It allows users to organize and share their information and online resources on the Web (Li,...
Pointer Programs and Undirected Reachability ∗ (2009)
We study pointer programs as a model of structured computation within logspace. Pointer programs capture the common description of logspace algorithms as programs that take as input some structured...
On the non-sequential nature of the interval-domain model of real-number computation (2008)
Martín Escardó, Martin Hofmann, Thomas Streicher
of real-number computation
Chapter 14 Project Evaluation Paper: Mobile Resource Guarantees (2008)
Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Ian Stark, Lennart Beringer, ...
Abstract: The Mobile Resource Guarantees (MRG) project has developed a proof-carrying-code infrastructure for certifying resource bounds of mobile code. Key components of this infrastructure are a...
Mobile Resource Guarantees Evaluation Paper (2008)
Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Lennart Beringer, Hans-wolfgang Loidl, ...
This paper summarises the main outcomes of the Mobile Resource Guarantees (MRG) project, a three year project funded by the EC under the FET proactive initiative on Global Computing, and discusses...
Adaptive Peer-toPeer Agent Sensor Networks (2008)
Ray-yuan Sheu, Michael Czajkowski, Martin Hofmann
We present an agent-based, adaptive peer-to-peer, hybrid architectural approach for sensor networks to address some of the challenges and needs presented in net-centric, field-deployed, or...
Chapter 1 Mobile Resource Guarantees Evaluation Paper (2008)
Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Ian Stark, Lennart Beringer, ...
Abstract: The Mobile Resource Guarantees (MRG) project has developed a proof-carrying-code infrastructure for resources to be applied to mobile code. Key components of this infrastructure are a...
Inductive Synthesis of Recursive Functional Programs A Comparison of Three Systems (2008)
Martin Hofmann, Andreas Hirschberger, Emanuel Kitzelmannn
One of the most challenging subfields, and a still little researched niche of machine learning, is the inductive synthesis of recursive programs from incomplete specifications, such as examples for...
Reading, Writing and Relations Towards Extensional Semantics for Effect Analyses (2008)
Nick Benton, Andrew Kennedy, Martin Hofmann, Lennart Beringer
Abstract. We give an elementary semantics to an effect system, tracking read and write effects by using relations over a standard extensional semantics for the original language. The semantics...
Toward Interoperability of Mobile-Agent Systems (2008)
Arne Grimstrup, Robert Gray, David Kotz, Maggie Breedy, Marco Carvalho, Thomas Cowin, ...
Abstract. Growing recognition of the benefits of mobile agents in distributed systems, such as military C4ISR, has led to a proliferation of mobile agent systems. However, incompatibilities between...
Andrea Christen, Martin Hofmann
The students of the university of teacher education St.Gallen (PHSG, Switzerland) document aspects of their learning process affiliated with their first experiences in a practical training class...
Kevin Hammond, Roy Dyckhoff, Christian Ferdin, Martin Hofmann, Steffen Jost, Andy Wallace
e1.3M project that will develop static analyses for resource-bounded computations (both space and time) in real-time embedded systems using the domainspecific language Hume,a language that combines...
Agents and Robots Teaming With People — A New Strategy for Cognitive Systems Research (2008)
Kenneth Whitebread, Lori Pridmore, Martin Hofmann, Anna Buczak
We propose an alternative approach to cognitive system research based on the concept of a “cognitive team system ” composed of interacting humans and “active computational systems ” (ACSs)...
2001, ‘A Higher-Order Embedding of a Logic of Objects (2008)
Abstract. We present an implementation of a program logic of objects, extending that (AL) of Abadi and Leino. In particular, the implementation uses higher-order abstract syntax (HOAS) and—unlike...
Finite Dimensional Vector Spaces are Complete for Traced Symmetric Monoidal Categories (2008)
Masahito Hasegawa, Martin Hofmann, Gordon Plotkin
Abstract. We show that the category FinVectk of finite dimensional vector spaces and linear maps over any field k is (collectively) complete for the traced symmetric monoidal category freely...
Chapter 1 Mobile Resource Guarantees Evaluation Paper (2008)
Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Ian Stark, Lennart Beringer, ...
Abstract: This paper summarises the main outcomes of the Mobile Resource Guarantees (MRG) project, which focused on a proof-carrying-code (PCC) infrastructure for resources to be applied to mobile...
Anna Bucalo, Martin Hofmann, Furio Honsell, Marino Miculan, Ivan Scagnetto
The Theory of Contexts is a type-theoretic axiomatization aiming to give a metalogical account of the fundamental notions of variable and context as they appear in Higher Order Abstract Syntax. In...
Completeness of continuation models for (2008)
Synopsis We show that a certain simple call-by-name continuation semantics of Parigot's *_-calculus is complete. More precisely, for every *_-theory we construct a cartesian closed category such...
Reading, Writing and Relations Towards Extensional Semantics for Effect Analyses (2008)
Nick Benton, Andrew Kennedy, Martin Hofmann, Lennart Beringer
Abstract. We give an elementary semantics to an effect system, tracking read and write effects by using relations over a standard extensional semantics for the original language. The semantics...
Towards Formally Verifiable WCET Analysis for a Functional Programming Language (2008)
Kevin Hammond, Christian Ferdin, Martin Hofmann, Steffen Jost, Hans-wolfgang Loidl, ...
Towards Formally Verifiable WCET Analysis for a Functional Programming Language (2008)
Kevin Hammond, Christian Ferdinand, Reinhold Heckmann, Roy Dyckhoff, Martin Hofmann, ...
This paper describes ongoing work aimed at the construction of formal cost models and analyses to yield verifiable guarantees of resource usage in the context of real-time embedded systems. Our work...
Andrea Christen, Martin Hofmann
The students of the university of teachereducation St.Gallen (PHSG, Switzerland) document aspectsof their learning process affiliated with their firstexperiences in a practical training class during...
08061 Executive Summary -- Types, Logics and Semantics for State (2008)
Ahmed, Amal, Benton, Nick, Hofmann, Martin, Morrisett, Greg
From 3 February to 8 February 2008, the Dagstuhl Seminar 08061 Stateââ¬Â Conference and Research Center (IBFI), Schloss Dagstuhl. 45 researchers, with interests and expertise in many...
08061 Abstracts Collection -- Types, Logics and Semantics for State (2008)
Ahmed, Amal, Benton, Nick, Hofmann, Martin, Morrisett, Greg
From 3 February to 8 February 2008, the Dagstuhl Seminar 08061 ``Types, Logics and Semantics for State'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During...
In-place update with linear types or How to compile functional programs into malloc()-free C (2007)
this paper is to show that by imposing mild extra annotations one can have the best of both worlds: easy to write code which is amenable to equational reasoning, yet modifies its arguments in place...
Robert S. Gray, David Kotz, Joyce Barton, Peter Gerken, Martin Hofmann
Abstract. Building applications with mobile agents often reduces the bandwidth required for the application, and improves performance. The cost is increased server workload. There are, however, few...
Generation of verification conditions for Abadi and Leino's Logic of Objects (2007)
Extended Abstract, Francis Tang, Martin Hofmann
de We consider the problem of verification condition generation for Abadi and Leino's program logic (AL) for objects. We provide an algorithm which to a given judgement J in AL computes a...
Martin Hofmann, Benjamin Pierce
We give a direct type-theoretic characterization of the basic mechanisms of object-oriented programming, including objects, methods, message passing, and subtyping, by introducing an explicit...
Martin Hofmann, Donald Sannella
behavioural abstraction and behavioural satisfaction
Toward Dynamic Interoperability of Mobile-Agent Systems (2007)
Arne Grimstrup, Robert Gray, David Kotz, Maggie Breedy, Marco Carvalho, Thomas Cowin, ...
Abstract. Mobile agents are an increasingly popular paradigm and in recent years there has been a proliferation of mobile-agent systems. These systems are, however, largely incompatible with each...
Robert S. Gray, David Kotz, Joyce Barton, Peter Gerken, Martin Hofmann
, and Niranjan Suri 3 1
2001, ‘A Higher-Order Embedding of a Logic of Objects (2007)
Martin Hofmann, Martin Hofmann, Martin Hofmann, Francis Tang, Francis Tang, Francis Tang
We present an implementation of a program logic of objects, extending that (AL) of Abadi and Leino. In particular, the implementation uses higher-order abstract syntax (HOAS) and—unlike previous...
Klaus Aehlig, Ulrich Berger, Martin Hofmann
arithmetic for non-size-increasing polynomial-time computation
Header Body Footer Margin Notes (2007)
Abstract: We present a type inference algorithm for the underlying language and type system of a logic (AL [2]) of Abadi and Leino. We approach the problem by following the techniques used by...
2001, ‘A Higher-Order Embedding of a Logic of Objects (2007)
Abstract. We present an implementation of a program logic of objects, extending that (AL) of Abadi and Leino. In particular, the implementation uses higher-order abstract syntax (HOAS) and---unlike...
Thorsten Altenkirch, Thomas Streicher, Martin Hofmann, Martin Hofmann
Reduction-free normalisation for system F Address for correspondence:
DRAFT: Type Inference for Object Types with Base Types (2007)
We consider an object calculus of Abadi and Leino. The language has a type system with object subtyping which allows for specialisation, covariant subtyping in the return types of methods and...
An Arithmetic for Non-Size-Increasing Polynomial-Time Computation (2007)
Klaus Aehlig, Ulrich Berger, Martin Hofmann, Helmut Schwichtenberg
An arithmetical system is presented with the property that from every proof a realizing term can be extracted that is definable in a certain affine linear typed variant of Godel's T and...
David Aspinall, Martin Hofmann
Abstract. Linear typing schemes guarantee single-threadedness and so the soundness of in-place update with respect to a functional semantics. But linear schemes are restrictive in practice, and more...
Mobius: Mobility, ubiquity, security: Objectives and progress report (2007)
Gilles Barthe, Lennart Beringer, Pierre Crégut, Benjamin Grégoire, Martin Hofmann, Peter Müller, ...
Abstract. Through their global, uniform provision of services and their distributed nature, global computers have the potential to profoundly enhance our daily life. However, they will not realize...
Mobius: Mobility, ubiquity, security: Objectives and progress report (2007)
Gilles Barthe, Lennart Beringer, Pierre Crégut, Benjamin Grégoire, Martin Hofmann, Peter Müller, ...
Abstract. Through their global, uniform provision of services and their distributed nature, global computers have the potential to profoundly enhance our daily life. However, they will not realize...
Im Studiengang Wirtschaftsinformatik, Und Angewandte Informatik, Martin Hofmann, Prof Dr, Ute Schmid
This diploma thesis bridges the gap between fundamental research in Inductive Program Synthesis and its practical application for end user programming. It demonstrates that it is indeed feasible to...
Type-Based Amortised Heap-Space Analysis (2006)
Abstract. We present a type system for a compile-time analysis of heapspace requirements of Java style object-oriented programs with explicit deallocation. Our system is based on an amortised...
Towards formally verifiable resource bounds for real-time embedded systems (2006)
Kevin Hammond, Christian Ferdin, Reinhold Heckmann, Roy Dyckhoff, Martin Hofmann, Steffen Jost, ...
This paper describes ongoing work aimed at the construction of formal cost models and analyses that are capable of producing verifiable guarantees of resource usage (space, time and ultimately power...
A proof system for the linear time µ-calculus (2006)
Christian Dax, Martin Hofmann, Martin Lange
Abstract. The linear time μ-calculus extends LTL with arbitrary least and greatest fixpoint operators. This gives it the power to express all ω-regular languages, i.e. strictly more than LTL. The...
A proof system for the linear time µ-calculus (2006)
Christian Dax, Martin Hofmann, Martin Lange
Abstract. The linear time µ-calculus extends LTL with arbitrary least and greatest fixpoint operators. This gives it the power to express all ω-regular languages, i.e. strictly more than LTL. The...
Christoph M. Friedrich, Thomas Revillion, Martin Hofmann, Juliane Fluck
We present our work on Chemical and Biomedical Named Entity Recognition (NER) using Machine Learning algorithms with different feature sets. It will be demonstrated, that the best results could be...
Zugl.: Göttingen, Univ., Diss., 2005.
Automatic Certification of Heap Consumption (2005)
Lennart Beringer, Martin Hofmann, Alberto Momigliano, Olha Shkaravska
Abstract. We present a program logic for verifying the heap consumption of low-level programs. The proof rules employ a uniform assertion format and have been derived from a general purpose program...
Mobile Resource Guarantees for Smart Devices (2005)
David Aspinall, Stephen Gilmore, Martin Hofmann, Donald Sannella, Ian Stark
Abstract. We present the Mobile Resource Guarantees framework: a system for ensuring that downloaded programs are free from run-time violations of resource bounds. Certificates are attached to code...
Mobile Resource Guarantees for Smart Devices (2005)
David Aspinall, Stephen Gilmore, Martin Hofmann, Donald Sannella, Ian Stark
Abstract. We present the Mobile Resource Guarantees framework: a system for ensuring that downloaded programs are free from run-time violations of resource bounds. Certificates are attached to code...
Mobile Resource Guarantees for Smart Devices (2005)
David Aspinall, Stephen Gilmore, Martin Hofmann, Donald Sannella
Abstract. We present the Mobile Resource Guarantees framework: a system for ensuring that downloaded programs are free from run-time violations of resource bounds. Certificates are attached to code...
04381 Abstracts Collection -- Dependently Typed Programming (2005)
Altenkirch, Thorsten, Hofmann, Martin, Hughes, John
From 12.09.04 to 17.09.04, the Dagstuhl Seminar 04381 ``Dependently Typed Programming'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar,...
Title from Box
Towards certificate generation for linear heap consumption (2004)
Lennart Beringer, Martin Hofmann, Alberto Momigliano, Olha Shkaravska
representation of the Java virtual machine language. The logic is defined by an expansion into the more general level, without recourse to the base logic. Format and interpretation of assertions...
A Program Logic for Resource Verification (2004)
David Aspinall, Lennart Beringer, Martin Hofmann, Hans-wolfgang Loidl, Alberto Momigliano
We present a program logic for reasoning about resource consumption of programs written in Grail, an abstract fragment of the Java Virtual Machine Language. Serving as the target logic of a...
Managing a portal of digital web resources by content syndication (2003)
Vet Van Der, Paul, Hofmann, Martin, Huibers, Theo, Roosendaal, Hans
As users become more accustomed to continuous Internet access, they will have less patience with the offering of disparate resources. A new generation of portals is being designed that aids users in...
Static Prediction of Heap Space Usage for First-Order Functional Programs (2003)
We show how to eciently obtain linear a priori bounds on the heap space consumption of rst-order functional programs. The analysis takes space reuse by explicit deallocation into account and also...
Darstellung asymmetrischer P-C-Käfigverbindungen / (2003)
Erlangen, Nürnberg, Universiẗat, Diss., 2003.
Space and time dependence of temperature and freezing in evergreen leaves (2002)
Ball, Marilyn, Canny, Martin, Hofmann, Martin, Nicotra, Adrienne, Hughes, Dale
Infrared video thermography was used to study space and time dependence of freezing in intact, attached leaves of snow gum (Eucalyptus pauciflora Sieb. ex Spreng.) seedlings. Freezing initiated in...
Generation of verification conditions for abadi and leino’s logic of objects (2002)
We consider the problem of verification condition generation for Abadi and Leino's program logic (AL) for objects. We provide an algorithm which to a given judgement J in AL computes a formula...
Another type system for in-place update (2002)
David Aspinall, Martin Hofmann
Abstract. Linear typing schemes guarantee single-threadedness and so the soundness of in-place update with respect to a functional semantics. But linear schemes are restrictive in practice, and more...
On the Non-Sequential Nature of (2002)
Martin Hofmann, Thomas Streicher
We show that real-number computations in the interval-domain environment are \inherently parallel" in a precise mathematical sense. We do this by reducing computations of the weak parallel-or...
Mobile-Agent versus Client/Server Performance: Scalability in an Information-Retrieval Task (2001)
Robert S. Gray, David Kotz, Ronald A. Peterson, Peter Gerken, Martin Hofmann, Daria Chacon, ...
Mobile agents are programs that can jump from host to host in the network, at times and to places of their own choosing. Many groups have developed mobile-agent software platforms, and several...
Write once, move anywhere: Toward dynamic interoperability of mobile agent systems (2001)
Arne Grimstrup, Robert Gray, David Kotz, Martin Hofmann
Mobile agents are an increasingly popular paradigm, and in recent years there has been a proliferation of mobile-agent systems. These systems are, however, largely incompatible with each other. In...
Robert S. Gray, David Kotz, Ronald A. Peterson, Peter Gerken, Martin Hofmann, Daria Chacón, ...
Mobile agents are programs that can jump from host to host in the network, at times and to places of their own choosing. Many groups have developed mobile-agent software platforms, and several...
Reducing proof burden in object-oriented verification (2001)
We consider for an object-oriented language, a verication condition generator (VCG), a tool which assists the programmer in proving program correctness. The tool automatically discharges those parts...
Consistency of the Theory of Contexts (2001)
Anna Bucalo, Martin Hofmann, Furio Honsell, Marino Miculan, Ivan Scagnetto
The Theory of Contexts is a type-theoretic axiomatization which has been recently proposed by some of the authors for giving a metalogical account of the fundamental notions of variable and context...
Normalization by Evaluation for Typed Lambda Calculus with Coproducts (2001)
Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, Philip Scott, P. Scott
We solve the decision problem for simply typed lambda calculus with strong binary sums, equivalently the word problem for free cartesian closed categories with binary coproducts. Our method is based...
Mobile-Agent versus Client/Server Performance: Scalability in an Information-Retrieval Task (2001)
Robert S. Gray, David Kotz, Ronald A. Peterson, Peter Gerken, Martin Hofmann, Daria Chacón, ...
Mobile agents are programs that can jump from host to host in the network, at times and to places of their own choosing. Many groups have developed mobile-agent software platforms, and several...
A New "Feasible" Arithmetic (2000)
A classical quantified modal logic is used to define a "feasible" arithmetic A 1 2 whose provable functions are exactly the polynomial-time computable functions. Informally, one understands...
Safe recursion with higher types and BCK-algebra (2000)
In previous work the author has introduced a lambda calculus SLR with modal and linear types which serves as an extension of Bellantoni-Cook's function algebra BC to higher types. It is a step...
Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover (2000)
. We present an implementation of a program logic of objects, extending that (AL) of Abadi and Leino. In particular, the implementation uses higher-order abstract syntax (HOAS) and---unlike previous...
this article is to survey this development beginning from Cobham's 1965 result which was the rst in the area, up to the current research frontier.
A type system for bounded space and functional in-place update (Extended Abstract) (2000)
Martin Hofmann LFCS Edinburgh, Mayfield Rd, Edinburgh EH9 3JZ, UK mxh@dcs.ed.ac.uk Abstract. We show how linear typing can be used to obtain functional programs which modify heap-allocated data...
A New "Feasible " Arithmetic (2000)
Abstract A classical quantified modal logic is used to define a "feasible " arithmetic A12 whose provable functions are exactly the polynomial-time computable functions. Informally,...
Implementing a program logic of objects in a higher-order logic theorem prover (2000)
Abstract. We present an implementation of a program logic of objects, extending that (AL) of Abadi and Leino. In particular, the implementation uses higher-order abstract syntax (HOAS) and—unlike...
Type Systems For Polynomial-time Computation (1999)
This thesis introduces and studies a typed lambda calculus with higher-order primitive recursion over inductive datatypes which has the property that all definable number-theoretic functions are...
Type Systems For Polynomial-time Computation (1999)
This thesis introduces and studies a typed lambda calculus with higher-order primitive recursion over inductive datatypes which has the property that all definable number-theoretic functions are...
Linear types and non-size-increasing polynomial time computation (1999)
Synopsis: We propose a linear type system with recursion operators for inductive datatypes which ensures that all definable functions are polynomial time computable. The system improves upon previous...
Semantical Analysis of Higher-Order Syntax (1999)
this paper to advocate the use of functor categories as a semantic foundation of higher-order abstract syntax (HOAS). By way of example, we will show how functor categories can be used for at least...
Multi-Agent Common Operating Environment (MACOE) (1998)
Whitebread, Ken, Hofmann, Martin, Pridmore, Lori
The Multi-Agent Common Operating Environment is an effort funded under the CoABS program executed by prime contractor Lockheed Martin Advanced Technology Labs (LM ATL). ATL's mission under the CoABS...
Intelligent Interoperable Agent Toolkit (I2AT) (1998)
The challenge on this effort has been how to transition current agent technology in such a way that it is widely deployed. To date, building useful agent applications for C41SR has required...
Effect of Ionic Substitution on the Thermal Expansion of ZrTiO4. (1998)
Bayer, Gerhard, Hofmann, Martin, Gauckler, Ludwig J.
Polycrystalline AlN bodies were made with a range of porosities from various AlN powders by sintering or hot-pressing. Thermal conductivity data for material produced without sintering aids showed a...
München, Univ., Diss., 1998.
Martin Hofmann, Benjamin C. Pierce
We study a variant of System F that integrates and generalizes several existing proposals for calculi with structural typing rules. To the usual type constructors (!, \Theta, All, Some, Rec) we add a...
Linear Types and Non-Size-Increasing Polynomial Time Computation (1998)
We propose a linear type system with recursion operators for inductive datatypes which ensures that all denable functions are polynomial time computable. The system improves upon previous such...
A mixed modal/linear lambda calculus with applications to Bellantoni-Cook safe recursion (1998)
. This paper introduces a simply-typed lambda calculus with both modal and linear function types. Through the use of subtyping extra term formers associated with modality and linearity are avoided....
Type Systems For Polynomial-Time Computation (1998)
Martin Hofmann, Martin Hofmann Phd
This thesis introduces and studies a typed lambda calculus with higher-order primitive recursion over inductive datatypes which have the property that all definable number-theoretic functions are...
Semantics of Linear/modal Lambda Calculus (1998)
In previous work the author has introduced a lambda calculus SLR with modal and linear types which serves as an extension of Bellantoni-Cook's function algebra BC to higher types. It is a step...
Martin Hofmann, Type Destructors, Benjamin C. Pierce
We study a variant of System F that integrates and generalizes several existing proposals for calculi with structural typing rules. To the usual type constructors (!, , All, Some, Rec) we add anumber...
Continuation models are universal for -calculus (1997)
Abstract We show that a certain simple call-by-name continuation semantics of Parigot's *_-calculus is complete. More precisely, for every *_-theory we construct a cartesian closed category such...
Syntax and Semantics of Dependent Types (1997)
ion is written as [x: oe]M instead of x: oe:M and application is written M(N) instead of App [x:oe] (M; N ). 1 Iterated abstractions and applications are written [x 1 : oe 1 ; : : : ; x n : oe n ]M...
Martin Hofmann, Martin Hofmann Darmstadt
We use the category of presheaves over PTIME-functions in order to show that Cook and Urquhart's higher-order function algebra PV ! defines exactly the PTIME-functions. As a byproduct we obtain...
Martin Hofmann, Benjamin Pierce
The statement S T in a-calculus with subtyping is traditionally interpreted as a semantic coercion function of type [[S]]![[T]] that extracts the "T part " of an element of S. If...
The Groupoid Interpretation of Type Theory (1996)
Martin Hofmann, Thomas Streicher
ion and application Suppose that M 2 Tm(B). We define its abstraction A;B (M) 2 Tm(\Pi LF (A; B)) on objects by A;B (M)(fl)(a) = M(fl; a) A;B (M)(fl)(q) = M(id fl ; q) If p : fl ! fl 0 then we need a...
Martin Hofmann, Wolfgang Naraschewski, Martin Steffen, Terry Stroup, Fachbereich Mathematik
The Curry--Howard isomorphism, a fundamental property shared by many type theories, establishes a direct correspondence between programs and proofs. This suggests that the same structuring principles...
Reduction-Free Normalisation for a Polymorphic System (1996)
Thorsten Altenkirch, Martin Hofmann, Thomas Streicher
We give a semantic proof that every term of a combinator version of system F has a normal form. As the argument is entirely formalisable in an impredicative constructive type theory a reduction-free...
On behavioural abstraction and behavioural satisfaction in higher-order logic (1996)
Martin Hofmann, Donald Sannella
The behavioural semantics of specifications with higher-order logical formulae as axioms is analyzed. A characterization of behavioural abstraction via behavioural satisfaction of formulae in which...
On behavioural abstraction and behavioural satisfaction in higher-order logic (1996)
Martin Hofmann, Donald Sannella
The behavioural semantics of specifications with higher-order logical formulae as axioms is analyzed. A characterization of behavioural abstraction via behavioural satisfaction of formulae in which...
The Groupoid Interpretation of Type Theory (1996)
Martin Hofmann, Thomas Streicher
this paper we answer the question of derivability of UIP in pure type theory in the negative by exhibiting a counter model. By the above, this model does not validate pattern matching thereby...
Extensional concepts in intensional type theory (1995)
Theories of dependent types have been proposed as a foundation of constructive mathematics and as a framework in which to construct certified programs. In these applications an important role is...
Extensional concepts in intensional type theory (1995)
Theories of dependent types have been proposed as a foundation of constructive mathematics and as a framework in which to construct certified programs. In these applications an important role is...
Konzeption eines Prozessinformations- und -managementsystems / (1995)
Zugl.: Zürich, Techn. Hochsch., Diss., 1995.
Konzeption eines prozessinformations- und -managementsystems [microform] / (1995)
Thesis (doctoral)--Eidgenössische Technische Hochschule Zürich, 1995.
On Behavioural Abstraction and Behavioural Satisfaction in Higher-Order Logic (1995)
Martin Hofmann, Donald Sannella
The behavioural semantics of specifications with higher-order logical formulae as axioms is analyzed. A characterization of behavioural abstraction via behavioural satisfaction of formulae in which...
Categorical Reconstruction of a Reduction Free Normalization Proof (1995)
Thorsten Altenkirch, Martin Hofmann, Thomas Streicher
Introduction We present a categorical proof of the normalization theorem for simply typed -calculus, i.e. we derive a computable function nf which assigns to every typed -term a normal form, s.t. M...
A Simple Model for Quotient Types (1995)
. We give an interpretation of quotient types within in a dependent type theory with an impredicative universe of propositions (Calculus of Constructions). In the model, type dependency arises only...
Martin Hofmann, Benjamin Pierce
this paper, we have assigned meaning to terms by giving a PER model providing both a simple operational semantics and justification of a set of equational rules. For larger calculi (including, for...
Sound and Complete Axiomatisations of Call-By-Value Control Operators (1994)
ion. Let \Gamma; x : oe ` M : ø . [[x : oe:M ]] = : (oe * ø ) * 0: (x : oe:M ) = by C-App : (x:C ø (k : ø * 0:k M )) = : (x:C ø ([[M ]])) = j oe*ø (x:C([[M ]])) which is the required expression...
On the Interpretation of Type Theory in Locally Cartesian Closed Categories (1994)
. We show how to construct a model of dependent type theory (category with attributes) from a locally cartesian closed category (lccc). This allows to define a semantic function interpreting the...
A Unifying Type-Theoretic Framework for Objects (1993)
Martin Hofmann, Benjamin Pierce
We give a direct type-theoretic characterization of the basic mechanisms of object-oriented programming, including objects, methods, message passing, and subtyping, by introducing an explicit...
Splicing choice from ten variant exons establishes CD44 variability (1993)
Tölg, Cornelia, Hofmann, Martin, Herrlich, Peter, Ponta, Helmut
The enormous heterogeneity of the surface protein designated CD44 is in part due to posttranslational modification, and in part due to differential splicing. Alternative splicing occurs within one...
Ueber Zusammengesetzte Poisson-Prozesse und ihre Anwendungen in der Unfallversicherung. (1955)
Zürich, Eidg. Techn. H., Diss.
Weiss, Johannes M., Sleeman, Jonathan, Renkl, Andreas C., Dittmar, Henning, Termeer, Christian C., Taxis, Sabine, ...
Upon antigen contact, epidermal Langerhans cells (LC) and dendritic cells (DC) leave peripheral organs and home to lymph nodes via the afferent lymphatic vessels and then assemble in the paracortical...
ESF Workshop on ‘Sustainability and Governance of Web and GRID Resources in Functional Genomics’
Van Der Vet, Paul, Huibers, Theo, Binz, Pierre-Alain, Hofmann, Martin
A New Method for Establishing Conservativity of Classical Systems Over Their Intuitionistic Version
Thierry Coquand, Martin Hofmann
this paper we present such a method. Applied to I \Sigma
Martin Hofmann, Copyright C, Martin Hofmann
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent BRICS...