Integrating Logic with Partial Functions into a Proof Checker In 2010-2013 I developed a 3-valued logic for Partial Functions. During 2013-2014, I tried to integrate this logic into an interactive proof checker. It was unsuccesful. (The resulting proof checker was too unpleasant to use.) In this talk, I summarize a new attempt, which has not been implemented yet: - I explain basics of the underlaying 3-valued logic. - How to generalize this logic to higher-order. - How to build theories (using little theory). Theories can be substantive or adjective in nature. - Type Reductions. Explicit type conditions are useful, but very unpleasant in practical use.