[Přednáška je z důvodu nemoci zrušena a přesunuta do letního semestru]  Vít Punčochář (Filozofický ústav AVČR) bude mluvit na semináři 5.1.2025, 16:40. Název: Truthmaker Semantics and Curry-Howard Correspondence, Abstract: Kit Fine characterized his truthmaker semantics for intuitionistic logic as a “cross between the construction-oriented semantics of Brouwer–Heyting–Kolmogorov and the condition-oriented semantics of Kripke.” While the relation to Kripke semantics is well understood, the connection to construction-oriented, type-theoretic frameworks that more directly implement the BHK interpretation has remained less clear. In this talk, I clarify this relationship by developing a truthmaker semantics for the simply typed lambda calculus with products and sums. The resulting framework provides a fully compositional interpretation of proofs and derivations within the algebra of truthmakers.