Basil A. KarádaisArbeitsgruppe Mathematische Logik
Mathematisches Institut der Universität München Email: karadais at math dot lmu dot de Tel: +49 (0)89 2180 4417 Sprechstunde: nach Vereinbarung 

Work
Highertype computability theory, Denotational semantics of programming languages, Constructive domain theory
(older webpage).
 Nonflatness and totality (submitted)
LMU 2016
Abstract. We prove a strong version of the Kreisel density theorem by providing a witness generated by a compact element. This is achieved by interpreting finite types as domains over nonflat base types. Separation is obtained as a corollary, and the mismatch of the nonflat and flatbased versions of totality is discussed.
 Normal forms, linearity, and prime algebraicity over nonflat domains (submitted)
UNIPD 2015
Abstract. Using representations of nonflatbased Scott domains to model type systems, it is natural to wish that they be "linear", in which case the complexity of the fundamental test for entailment of information drops from exponential to linear, the corresponding mathematical theory becomes much simpler, and moreover has ties to models of computation arising in the study of sequentiality, concurrency, and linear logic. Earlier attempts to develop a fully nonflat semantics based on linear domain representations for a rich enough type system allowing inductive types, were designed in a way that felt rather artificial, as it featured certain awkward and counterintuitive properties; eventually, the focus turned on general, nonlinear representations.
Here we try to turn this situation around, by showing that we can work linearly in a systematic way within the nonlinear model, and that we may even restrict to a fully linear model whose objects are in a bijective correspondence with the ones of the nonlinear and are easily seen to form a prime algebraic domain. To obtain our results we study mappings of finite approximations of objects that can be used to turn approximations into normal and linear forms.
Outline (talk)
UNIPD 04.02.2015
Slides (talk)
Bridges between financial and constructive mathematics 2015
 Atomicity, coherence of information, and pointfree structures (preprint)
Annals of Pure and Applied Logic 167, pp. 753769, 2016
Abstract. We prove basic facts about the properties of atomicity and coherence for Scott information systems, and we establish direct connections between coherent information systems and wellknown pointfree structures.
 Implicit atomicity and finite density for nonflat domains (preprint)
LMU 2013
Abstract. The KleeneKreisel density theorem states that total ideals are dense in the finitely generated partial ideals of a given type. We investigate the status of this statement for nonflat domains, through their representation as nonflat coherent Scott information systems, in an internal, bottomup approach. We prove that such information systems are implicitly atomic, in the sense that, at each type, a neighborhood has an equivalent one whose closure is atomic, and use this fact to provide finite witnesses for density and separation.
Note. This work has meanwhile been substantially superseded by more recent work, see "Normal forms, linearity, and prime algebraicity over nonflat domains" and "Nonflatness and totality" above.
 Towards an arithmetic for partial computable functionals (phd thesis)
LMU 2013
Abstract. The thesis concerns itself with nonflat Scott information systems as an appropriate denotational semantics for the proposed theory \( \mathrm{TCF}^+ \), a constructive theory of highertype partial computable functionals and approximations. We prove a definability theorem for type systems with at most unary constructors via atomiccoherent information systems, and give a simple proof for the density property for arbitrary finitary type systems using coherent information systems. We introduce the notions of token matrices and eigenneighborhoods, and use them to locate normal forms of neighborhoods, as well as to demonstrate that even nonatomic information systems feature implicit atomicity. We then establish connections between coherent information systems and various pointfree structures. Finally, we introduce a fragment of \( \mathrm{TCF}^+ \) and show that extensionality can be eliminated.
Outline of the defense talk (talk)
LMU 12.08.2013  Atomicity in nonatomic information systems (talk)
Foundation of mathematics for computeraided formalization 2013  Recognizing tokens in a finitary algebra (unpublished) (a theorem of Schröter, Gerneth & Hall)
LMU 2012
Abstract. I describe here a technique of recognizing in linear time trees over a free algebra given by constructors. The technique is arithmetical rather than automata theoretic, in that it depends on the arities of the constructors rather than on their names.
Note. The main observation in the text (Proposition, p. 3) is Theorem 2.3, part III, in P. M. Cohn's Universal algebra (1981), or Theorem 1 in Chapter IV, Section 1, in C. Rosenbloom's Elements of mathematical logic (1950).
Following the references in these textbooks, we find that the idea was already known in the early 30's. Karl Menger ("Eine elementare Bemerkung über die Struktur logischer Formeln", Ergebnisse eines mathematischen Kolloquiums, vol. 3, 1930/31, pp. 22–3) had it in the context of Łukasiewicz' prefix notation for the propositional calculus (also called "polish notation"), for the case of an alphabet with unary and binary constructors—the intuition stemming from the negation and the logical connectives respectively. He thus derived a necessary and sufficient condition for a string to be a wellformed formula. Rosenbloom informs us that the same observation was independently made by Kazimierz Ajdukiewicz as well.
Karl Schröter ("Axiomatisierung der Fregeschen Aussagenkalküle", Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, neue Folge, Heft 8, 1943) discusses the case of arbitrary arities, as does Dal Charles Gerneth later, independently ("Generalization of Menger's result on the structure of logical formulas", Bulletin of the American Mathematical Society, vol. 54, 1948, pp. 803–804). Rosenbloom again informs us that Philip Hall, also independently, had made the same general observation; indeed, Hall talks about this "paradox of the pointlessness of punctuation" several years later, in his fairly wellknown address to the London Mathematical Society ("Some wordproblems", Journal of the London Mathematical Society, second series, vol. 33, 1958, pp. 482–496).
One can only admire the wonderful robustness of mathematical activity...
Manymany thanks to Magnus Steinby, who kindly referred me to Cohn's book seven months ago in January 2014. I've been meaning to update the text and pay the necessary dues all this time, but...
 Towards a formal theory of computability (preprint), with S. Huber and H. Schwichtenberg
Ways of proof theory (Pohler's festschrift), 2010
Abstract. We sketch a constructive formal theory \( \mathrm{TCF}^+ \) of computable functionals, based on the partial continuous functionals as their intended domain. Such a task had long ago been started by Dana Scott under the wellknown abbreviation \( \mathrm{LCF} \) (logic of computable functionals). The present approach differs from Scott's in two aspects.
(i) The intended semantical domains for the base types are nonflat free algebras, given by their constructors, where the latter are injective and have disjoint ranges; both properties do not hold in the flat case.
(ii) \(\mathrm{TCF}^+ \) has the facility to argue not only about the functionals themselves, but also about their finite approximations.
In this setting we give an informal proof (based on [Berger 1993]) of Kreisel's density theorem and an adaption of Plotkin's definability theorem. We then show that both proofs can be formalized in \( \mathrm{TCF}^+ \).
A case study (talk)
Arbeitstagung Bern–Munchen 2010  Plotkin definability theorem for atomiccoherent information systems (talk)
Computability in Europe 2008  Normal form of finite algebraic approximations (talk)
Seminar on proof theory WS 2006/7  Elaborating on Ishihara's 'WKL implies FAN' (talk)
EST training workshop 2005
Abstract. In 1990 Hajime Ishihara proved indirectly that the weak König's lemma implies the fan theorem. Here we reproduce a direct proof Ishihara provided for the same implication, which he presented in 2004 in Munich. This is a work done within a coordinated attempt of the Mathematical Logic Group in Munich to formalize Ishihara's arguments in theorem proving environments, an aim which was met in late spring by Stefan Schimanski on Coq and Nikolaus Thiel on Minlog.
See also at MathSciNet, Zentralblatt, and dblp.
Teaching

WS16/17: Single Variable Calculus

SS16: Differential and Integral Calculus II

WS15/16: Differential and Integral Calculus I

SS14: Programming and modeling
Functional programming in Haskell  WS13/14: Mathematical Logic

SS13: Logic and Discrete Structures
A dry, uncommented Mathematica file for the exercise A93: LDS13A93.nb (45KB).  WS12/13: Single Variable Calculus
 SS12: Logic and Discrete Structures
 WS11/12: Analysis I for students of Computer Science and Statistics
 WS10/11: Geometry
 SS10: Mathematical Logic II
 WS09/10: Linear Algebra for students of Computer Science and Statistics
 SS09: Synthetic and analytic treatment of geometric problems
 WS08/09: Differential and Integral Calculus III
 SS08 Complex Analysis (Funktionentheorie) (ss08_ft.rar, 2.5MB)
 SS07: Mathematical Logic II (ss07_mlii.rar, 390KB)
 SS05: Linear Algebra II
Last modified: 10.03.2017