OPUS 4 Latest Documents RSS FeedLatest documents
http://publikationen.stub.uni-frankfurt.de/index/index/
Tue, 15 Jul 2014 08:40:03 +0200Tue, 15 Jul 2014 08:40:03 +0200EU mapping: systematic overview on economic and financial legislation
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34447
In this study prepared for the ECON Committee of the European Parliament, Gellings, Jungbluth and Langenbucher present a graphic overview on core legislation in the area of economic and financial services in Europe. The mapping overview can serve as background for further deliberations. The study covers legislation in force, proposals and other relevant provisions in fourteen policy areas, i.e. banking, securities markets and investment firms, market infrastructure, insurance and occupational pensions, payment services, consumer protection in financial services, the European System of Financial Supervision, European Monetary Union, Euro bills and Coins and statistics, competition, taxation, commerce and company law, accounting and auditing.Marcel Gellings; Kai Jungbluth; Katja Langenbucherworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34447Tue, 15 Jul 2014 08:40:03 +0200Austerity, fiscal volatility, and economic growth
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34443
This paper contributes to the ongoing debate on the relationship between austerity measures and economic growth. We propose a general equilibrium model where (i) agents have recursive preferences; (ii) economic growth is endogenously driven by investments in R&D; (iii) the government is committed to a zero-deficit policy and finances public expenditures by means of a combination of labor taxes and R&D taxes. We find that austerity measures that rely on reducing resources available to the R&D sector depress economic growth both in the short- and long-run. High debt EU members are currently implementing austerity measures based on higher taxes and/or lower investments in the R&D sector. This casts some doubts on the real ability of these countries to grow over the next years.Giuliano Curatola; Michael Donadelli; Alessandro Gioffré; Patrick Grüningworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34443Mon, 14 Jul 2014 16:16:33 +0200Vertical fiscal imbalances and the accumulation of government debt : [Version Juli 2014]
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34454
The implications of delegating fiscal decision making power to sub-national governments has become an area of significant interest over the past two decades, in the expectation that these reforms will lead to better and more efficient provision of public goods and services. The move towards decentralization has, however, not been homogeneously implemented on the revenue and expenditure side: decentralization has materialized more substantially on the latter than on the former, creating "vertical fiscal imbalances". These imbalances measure the extent to which sub-national governments’ expenditures are financed through their own revenues. This mismatch between own revenues and expenditures may have negative consequences for public finances performance, for example by softening the budget constraint of sub-national governments. Using a large sample of countries covering a long time period from the IMF’s Government Finance Statistics Yearbook, this paper is the first to examine the effects of vertical fiscal imbalances on fiscal performance through the accumulation of government debt. Our findings suggest that vertical fiscal imbalances are indeed relevant in explaining government debt accumulation, and call for a degree of caution when promoting fiscal decentralization.Iñaki Aldasoro; Mike Seiferlingworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34454Mon, 14 Jul 2014 16:08:02 +0200Executive compensation structure and credit spreads : [Version 9 Juli 2014]
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34453
We develop a model of managerial compensation structure and asset risk choice. The model provides predictions about how inside debt features affect the relation between credit spreads and compensation components. First, inside debt reduces credit spreads only if it is unsecured. Second, inside debt exerts important indirect effects on the role of equity incentives: When inside debt is large and unsecured, equity incentives increase credit spreads; When inside debt is small or secured, this effect is weakened or reversed. We test our model on a sample of U.S. public firms with traded CDS contracts, finding evidence supportive of our predictions. To alleviate endogeneity concerns, we also show that our results are robust to using an instrumental variable approach.Stefano Colonnello; Giuliano Curatola; Ngoc Giang Hoangworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34453Mon, 14 Jul 2014 15:59:32 +0200Social security and the interactions between aggregate and idiosyncratic risk : [Version 9 Juli 2014]
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34452
We develop a model of managerial compensation structure and asset risk choice. The model provides predictions about how inside debt features affect the relation between credit spreads and compensation components. First, inside debt reduces credit spreads only if it is unsecured. Second, inside debt exerts important indirect effects on the role of equity incentives: When inside debt is large and unsecured, equity incentives increase credit spreads; When inside debt is small or secured, this effect is weakened or reversed. We test our model on a sample of U.S. public firms with traded CDS contracts, finding evidence supportive of our predictions. To alleviate endogeneity concerns, we also show that our results are robust to using an instrumental variable approach.Daniel Harenberg; Alexander Ludwigworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34452Mon, 14 Jul 2014 15:49:24 +0200Incompatible european partners? Cultural predispositions and household financial behavior
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34445
The Eurozone fiscal crisis has created pressure for institutional harmonization, but skeptics argue that cultural predispositions can prevent convergence in behavior. Our paper derives a robust cultural classification of European countries and utilizes unique data on natives and immigrants to Sweden. Classification based on genetic distance or on Hofstede’s cultural dimensions fails to identify a single ‘southern’ culture but points to a ‘northern’ culture. Significant differences in financial behavior are found across cultural groups, controlling for household characteristics. Financial behavior tends to converge with longer exposure to common institutions, but is slowed down by longer exposure to original institutions.Michael Haliassos; Thomas Jansson; Yigitcan Karabulutworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34445Mon, 14 Jul 2014 15:31:49 +0200Financial regulation in the EU - cross-border capital flows, systemic risk and the European Banking Union as reference points for EU financial market integration
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34444
This is a chapter for a forthcoming volume Oxford Handbook of Financial Regulation (Oxford University Press 2014) (eds. Eilís Ferran, Niamh Moloney, and Jennifer Payne). It provides an overview of EU financial regulation from the first banking directive up until its most recent developments in the aftermath of the financial crisis, focusing on the multiple layers of multi-level governance and their characteristic conceptual difficulties. Therefore the paper discusses the need to accommodate cross-border capital flows following from the EU internal market and the resulting regulatory strategies. This includes a brief overview of the principle of home country control and the ensuing Financial Services Action Plan. Dealing with the accommodation of cross-border capital flows and their regulation necessarily require an orchestration of the underlying supervisory structures, which is therefore also discussed. In the aftermath of the financial crisis of 2007-09 an additional aspect of necessary orchestration has emerged, that is the need to control systemic risk. Specific attention is paid to microprudential supervision by the newly established European Supervisory Authorities and macroprudential supervision in the European Banking Union, the latter’s underlying drivers and the accompanying Single Supervisory Mechanism, including the SSM’s institutional framework as well as the consideration of its rationales and the Single Resolution Mechanism closely linked to it.Brigitte Haarworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34444Mon, 14 Jul 2014 15:02:10 +0200Die Bankenabgabe in Deutschland - ein geeignetes Instrument zur Prävention von Finanzkrisen? : [Version April 2014?]
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34442
Helmut Siekmannworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34442Thu, 10 Jul 2014 15:03:47 +0200Die Entstehung des neuen Europäischen Finanzaufsichtssystems
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34441
ZUSAMMENFASSUNG UND ERGEBNISSE (1) Die Schaffung des Europäischen Ausschusses für Systemrisiken stößt nicht auf durchgreifende rechtliche Bedenken. (2) Es ist nicht sicher, dass die Errichtung der neuen Europäischen Aufsichtbehörden ohne entsprechende Änderung des Primärrechts zulässig ist. (3) Es kommt entscheidend darauf an, welche rechtsverbindlichen Einzelweisungsbefugnisse tatsächlich den Behörden verliehen werden. (4) Die nach dem Kompromiss vom 2. Dezember 2009 noch verbliebenen Einzelweisungsbefugnisse der Behörden gegenüber Privaten und gegenüber nationalen Aufsichtsbehörden sind rechtlich kaum abgesichert. (5) Wenn die hoheitlichen Befugnisse weitgehend oder vollständig beseitigt werden, bestehen Bedenken im Hinblick auf die Geeignetheit und Erforderlichkeit der Einrichtungen. (6) Die weitreichenden Unabhängigkeitsgarantien sind nicht mit den Anforderungen demokratischer Aufsicht und Kontrolle zu vereinbaren. (7) Für die Einräumung von Unabhängigkeit ist nach deutschem Verfassungsrecht eine ausdrückliche Regelung in der Verfassung, wie in Art. 88 Satz 2 GG, erforderlich. (8) Die transnationale Kooperation von Verwaltungsbehörden bedarf zumindest dann einer gesetzlichen Ermächtigung, wenn faktisch verbindliche Entscheidungen getroffen werden.Helmut Siekmannworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34441Thu, 10 Jul 2014 14:42:26 +0200The Single Supervisory Mechanism - Panacea or Quack Banking Regulation? : preliminary assessment of the evolving regime for the prudential supervision of banks with ECB involvement
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34202
Tobias Trögerworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34202Tue, 08 Jul 2014 16:44:28 +0200What happened in Cyprus? The economic consequences of the last communist government in Europe
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34319
This paper reviews developments in the Cypriot economy following the introduction of the euro on 1 January 2008 and leading to the economic collapse of the island five years later. The main cause of the collapse is identified with the election of a communist government in February 2008, within two months of the introduction of the euro, and its subsequent choices for action and inaction on economic policy matters. The government allowed a rapid deterioration of public finances, and despite repeated warnings, damaged the country's creditworthiness and lost market access in May 2011. The destruction of the island's largest power station in July 2011 subsequently threw the economy into recession. Together with the intensification of the euro area crisis in the summer and fall of 2011, these events weakened the banking system which was vulnerable due to its exposure in Greece. Rather than deal with its fiscal crisis, the government secured a loan from the Russian government that allowed it to postpone action until after the February 2013 election. Rather than protect the banking system, losses were imposed on banks and a campaign against them was coordinated and used as a platform by the communist party for the February 2013 election. The strategy succeeded in delaying resolution of the crisis and avoiding short-term political cost for the communist party before the election, but also in precipitating a catastrophe right after the election.Athanasios Orphanidesworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34319Tue, 08 Jul 2014 16:25:16 +0200Der makroprudenzielle Komplex: der Prozess, das Schloss, das Urteil
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34211
Hermann Remspergerworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34211Tue, 08 Jul 2014 16:13:15 +0200Correctness of an STM Haskell implementation
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34440
A concurrent implementation of software transactional memory in Concurrent Haskell using a call-by-need functional language with processes and futures is given. The description of the small-step operational semantics is precise and explicit, and employs an early abort of conflicting transactions. A proof of correctness of the implementation is given for a contextual semantics with may- and should-convergence. This implies that our implementation is a correct evaluator for an abstract specification equipped with a big-step semantics.Manfred Schmidt-Schauß; David Sabelworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34440Tue, 08 Jul 2014 15:04:26 +0200Towards correctness of program transformations through unification and critical pair computation
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34439
Correctness of program transformations in extended lambda calculi with a contextual semantics is usually based on reasoning about the operational semantics which is a rewrite semantics. A successful approach to proving correctness is the combination of a context lemma with the computation of overlaps between program transformations and the reduction rules, and then of so-called complete sets of diagrams. The method is similar to the computation of critical pairs for the completion of term rewriting systems.We explore cases where the computation of these overlaps can be done in a first order way by variants of critical pair computation that use unification algorithms. As a case study we apply the method to a lambda calculus with recursive let-expressions and describe an effective unification algorithm to determine all overlaps of a set of transformations with all reduction rules. The unification algorithm employs many-sorted terms, the equational theory of left-commutativity modelling multi-sets, context variables of different kinds and a mechanism for compactly representing binding chains in recursive let-expressions.Conrad Rau; Manfred Schmidt-Schaußworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34439Tue, 08 Jul 2014 14:56:08 +0200Reconstructing a logic for inductive proofs of properties of functional programs
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34438
David Sabel; Manfred Schmidt-Schaußworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34438Tue, 08 Jul 2014 14:44:41 +0200Reconstruction of a logic for inductive proofs of properties of functional programs
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34437
The interactive verification system VeriFun is based on a polymorphic call-by-value functional language and on a first-order logic with initial model semantics w.r.t. constructors. It is designed to perform automatic induction proofs and can also deal with partial functions. This paper provides a reconstruction of the corresponding logic and semantics using the standard treatment of undefinedness which adapts and improves the VeriFun-logic by allowing reasoning on nonterminating expressions and functions. Equality of expressions is defined as contextual equivalence based on observing termination in all closing contexts. The reconstruction shows that several restrictions of the VeriFun framework can easily be removed, by natural generalizations: mutual recursive functions, abstractions in the data values, and formulas with arbitrary quantifier prefix can be formulated. The main results of this paper are: an extended set of deduction rules usable in VeriFun under the adapted semantics is proved to be correct, i.e. they respect the observational equivalence in all extensions of a program. We also show that certain classes of theorems are conservative under extensions, like universally quantified equations. Also other special classes of theorems are analyzed for conservativity.David Sabel; Manfred Schmidt-Schaußworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34437Tue, 08 Jul 2014 14:35:53 +0200Reconstruction of a logic for inductive proofs of properties of functional programs
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34436
The interactive verification system VeriFun is based on a polymorphic call-by-value functional language and on a first-order logic with initial model semantics w.r.t. constructors. This paper provides a reconstruction of the corresponding logic when partial functions are permitted. Typing is polymorphic for the definition of functions but monomorphic for terms in formulas. Equality of terms is defined as contextual equivalence based on observing termination in all contexts. The reconstruction also allows several generalizations of the functional language like mutual recursive functions and abstractions in the data values. The main results are: Correctness of several program transformations for all extensions of a program, which have a potential usage in a deduction system. We also proved that universally quantified equations are conservative, i.e. if a universally quantified equation is valid w.r.t. a program P, then it remains valid if the program is extended by new functions and/or new data types.David Sabel; Manfred Schmidt-Schaußworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34436Tue, 08 Jul 2014 14:25:24 +0200On correctness of buffer implementations in a concurrent lambda calculus with futures
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34435
Motivated by the question of correctness of a specific implementation of concurrent buffers in the lambda calculus with futures underlying Alice ML, we prove that concurrent buffers and handled futures can correctly encode each other. Correctness means that our encodings preserve and reflect the observations of may- and must-convergence, and as a consequence also yields soundness of the encodings with respect to a contextually defined notion of program equivalence. While these translations encode blocking into queuing and waiting, we also describe an adequate encoding of buffers in a calculus without handles, which is more low-level and uses busy-waiting instead of blocking. Furthermore we demonstrate that our correctness concept applies to the whole compilation process from high-level to low-level concurrent languages, by translating the calculus with buffers, handled futures and data constructors into a small core language without those constructs.Jan Schwinghammer; David Sabel; Joachim Niehren; Manfred Schmidt-Schaußworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34435Tue, 08 Jul 2014 14:12:40 +0200Adequacy of compositional translations for observational semantics
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34433
We investigate methods and tools for analyzing translations between programming languages with respect to observational semantics. The behavior of programs is observed in terms of may- and mustconvergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extensions.Manfred Schmidt-Schauß; Joachim Niehren; Jan Schwinghammer; David Sabelworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34433Tue, 08 Jul 2014 14:02:58 +0200Adequacy of compositional translations for observational semantics
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34432
We investigate methods and tools for analyzing translations between programming languages with respect to observational semantics. The behavior of programs is observed in terms of may- and mustconvergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extensions.Manfred Schmidt-Schauß; Joachim Niehren; Jan Schwinghammer; David Sabelworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34432Tue, 08 Jul 2014 13:55:58 +0200Adequacy of compositional translations for observational semantics
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34431
We investigate methods and tools for analysing translations between programming languages with respect to observational semantics. The behaviour of programs is observed in terms of may- and mustconvergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extensions.
Manfred Schmidt-Schauß; Joachim Niehren; Jan Schwinghammer; David Sabelworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34431Tue, 08 Jul 2014 13:48:09 +0200Adequacy of compositional translations for observational semantics
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34430
We investigate methods and tools for analysing translations between programming languages with respect to observational semantics. The behaviour of programs is observed in terms of may- and mustconvergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extensions.Manfred Schmidt-Schauß; Joachim Niehren; Jan Schwinghammer; David Sabelworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34430Tue, 08 Jul 2014 13:41:34 +0200A finite simulation method in a non-deterministic call-by-need calculus with letrec, constructors and case
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34429
The paper proposes a variation of simulation for checking and proving contextual equivalence in a non-deterministic call-by-need lambda-calculus with constructors, case, seq, and a letrec with cyclic dependencies. It also proposes a novel method to prove its correctness. The calculus’ semantics is based on a small-step rewrite semantics and on may-convergence. The cyclic nature of letrec bindings, as well as nondeterminism, makes known approaches to prove that simulation implies contextual equivalence, such as Howe’s proof technique, inapplicable in this setting. The basic technique for the simulation as well as the correctness proof is called pre-evaluation, which computes a set of answers for every closed expression. If simulation succeeds in finite computation depth, then it is guaranteed to show contextual preorder of expressions.Manfred Schmidt-Schauß; Elena Machkasovaworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34429Tue, 08 Jul 2014 13:30:21 +0200On generic context lemmas for lambda calculi with sharing
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34428
This paper proves several generic variants of context lemmas and thus contributes to improving the tools for observational semantics of deterministic and non-deterministic higher-order calculi that use a small-step reduction semantics. The generic (sharing) context lemmas are provided for may- as well as two variants of must-convergence, which hold in a broad class of extended process- and extended lambda calculi, if the calculi satisfy certain natural conditions. As a guide-line, the proofs of the context lemmas are valid in call-by-need calculi, in callby-value calculi if substitution is restricted to variable-by-variable and in process calculi like variants of the π-calculus. For calculi employing beta-reduction using a call-by-name or call-by-value strategy or similar reduction rules, some iu-variants of ciu-theorems are obtained from our context lemmas. Our results reestablish several context lemmas already proved in the literature, and also provide some new context lemmas as well as some new variants of the ciu-theorem. To make the results widely applicable, we use a higher-order abstract syntax that allows untyped calculi as well as certain simple typing schemes. The approach may lead to a unifying view of higher-order calculi, reduction, and observational equality.Manfred Schmidt-Schauß; David Sabelworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34428Tue, 08 Jul 2014 13:09:22 +0200On generic context lemmas for lambda calculi with sharing
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34427
This paper proves several generic variants of context lemmas and thus contributes to improving the tools to develop observational semantics that is based on a reduction semantics for a language. The context lemmas are provided for may- as well as two variants of mustconvergence and a wide class of extended lambda calculi, which satisfy certain abstract conditions. The calculi must have a form of node sharing, e.g. plain beta reduction is not permitted. There are two variants, weakly sharing calculi, where the beta-reduction is only permitted for arguments that are variables, and strongly sharing calculi, which roughly correspond to call-by-need calculi, where beta-reduction is completely replaced by a sharing variant. The calculi must obey three abstract assumptions, which are in general easily recognizable given the syntax and the reduction rules. The generic context lemmas have as instances several context lemmas already proved in the literature for specific lambda calculi with sharing. The scope of the generic context lemmas comprises not only call-by-need calculi, but also call-by-value calculi with a form of built-in sharing. Investigations in other, new variants of extended lambda-calculi with sharing, where the language or the reduction rules and/or strategy varies, will be simplified by our result, since specific context lemmas are immediately derivable from the generic context lemma, provided our abstract conditions are met.Manfred Schmidt-Schauß; David Sabelworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/34427Tue, 08 Jul 2014 13:02:37 +0200