KAML
세미나

2017년

한국정보과학회 프로그래밍언어연구회 겨울학교 (SIGPL Winter School 2017)

  • 강연자: 허충길 (서울대학교), Martin Ziegler (KAIST)
  • 일시: 2017년 2월8일(수) ~ 2017년 2월10일(금)
  • 사전등록 마감: 2월 5일
  • 장소: KAIST 정보전자공학동(E3-1) 1층 제1공동강의실 (1501호)
  • 주최: 한국정보과학회 프로그래밍언어연구회
  • 주관: KAIST SW 중심 대학
  • 개요: 정형 증명 도구 Coq를 이용하여 논리학의 정리 증명 이론을 프로그래밍하고 실습합니다. 프로그래밍언어, 정형 기법, 시스템의 검증과 안전성, 그리고 전산학의 기초 이론 분야에 관심 있는 분들의 많은 참여 바랍니다.
  • 홈페이지: http://sigpl.or.kr/school/2017w

Kim-Independence and NSOP1 Theories

  • 강연자: Nick Ramsey (UC Berkeley)
  • 시간 및 장소: 2017년 1월 11일(수), 13일(금), 14:00 ~ 17:00 / 연세대학교 과학관 254호
  • 초록: The success of the theory of simple theories is built upon a number of theorems showing that forking has many desirable properties in a simple theory. Most of these properties, moreover, characterize simplicity (e.g., symmetry, transitivity, Kim's lemma), which means that a naïve generalization of these theorems to a broader class of theories is impossible. We will describe some recent work, now joint with Itay Kaplan, which shows that a simplicity-style structure theory exists for NSOP1 theories after replacing forking and dividing with their generic analogues, Kim- forking and Kim-dividing. This yields many new characterizations of NSOP1 theories and generalizes the known independence theory in several key examples.
  • 강연 슬라이드: 여기

2016년 2학기

Verification in Real Computation

  • 강연자: 박세원 (KAIST)
  • 시간 및 장소: 2016년 11월 4일, 금요일, 16:30 ~ 17:30시 / 연세대학교 과학관 263호
  • 초록: Using fundamental ideas from [Brattka&Hertling'98] and by means of object-oriented overloading of operators, the iRRAM library supports imperative programming over the reals with a both sound and computable, multivalued semantics of tests. We extend Floyd-Hoare Logic to formally verify the correctness of symbolic-numerical algorithms employing such primitives for three example problems: truncated binary logarithm, 1D simple root finding, and solving systems of linear equations. This is to be generalized to other hybrid (i.e. discrete and continuous) abstract data types.

  • 강연 슬라이드: 여기

Contemporary Model Theory

  • 강연자: Prof. Anand Pillay (Univ. of Notre Dame)

  • 시간 및 장소: 2016년 12월 16일, 금요일, 16:30 ~ 17:30시 / 연세대학교 과학관 262호
  • attachment:20161216_0.jpg

  • attachment:20161216_1.jpg

  • attachment:20161216_2.jpg

2016년 1학기

Logical Foundations of Efficient Validated Numerics

  • 강연자: Prof. Martin Ziegler (KAIST)

  • 시간 및 장소: 2016년 8월 26일, 금요일, 16:30 ~ 17:30시 / 연세대학교 과학관 262호
  • 초록: Recursive Analysis as the synthesis of computability theory and real analysis provides a sound foundation to Validated Numerics, that is, computation over real numbers and other continuous universes by approximation up to arbitrary guaranteed absolute error. In this talk I will recall its basic concepts and results before proceeding to its resource-bounded refinements, that is, address questions of algorithmic efficiency for real functions as investigated by Harvey Friedman, Ker-I Ko, Katrin Tent, and (the other) Martin Ziegler from Freiburg; I will conclude with recent own results about ordinary differential equations, about operators on analytic functions, and about computation on arbitrary compact metric spaces.
  • 강연 슬라이드: 여기

2015년 2학기

Frege's influence on modern practice of mathematics and logic

  • 강연자: 이계식 교수 (한경대학교)

  • 시간 및 장소: 2016년 2월 26일, 금요일, 17 ~ 18시 / 연세대학교 과학관 225호
  • 초록: This work started with the observation that, in Frege's work such as 'Begriffsschrift' and 'Basic Laws of Arithmetic', parameters (also called free variables) play essentially no role. And this drove us to check whether we could show the same meta-theoretic results even when we do not involve parameters to the language. We introduce a representation style of variable binding which is an important factor in doing formal proofs by using a computer. Our representation is a variation of the Coquand-McKinna-Pollack's locally-named representation. The main characteristic of our representation is the use of dependent families in defining expressions such as terms and formulas. We also show some hidden utility of simultaneous substitution and simultaneous renaming. Moreover, we could reveal a new aspect of locally-named representation style that it can be regarded as a nominal approach under the condition that proofs-as-programs is not a part of the domain of the discourse.

  • 강연 슬라이드: 여기

2015년 1학기

Point-free foundation of Mathematics

  • 강연자: Marco Benini 교수 (Università degli Studi dell’Insubria, 이탈리아)

  • 시간 및 장소: 2015년 7월 21일, 화요일, 16 ~ 17시 / 연세대학교 과학관 225호
  • 초록: In this talk, an alternative semantics for first-order, intuitionistic based theories is introduced. It main feature is to be "point-free", i.e., not requiring a universe where to interpret terms to exist. This semantics is sound and complete, and has many links with existing semantics. It fits into the paradigm "Correcteness by Construction" since it allows a direct computational interpretation of proofs along the lines of the propositions-as-types correspondence.
  • 강연 슬라이드: 여기

Mechanization of Proof: From 4-Color Theorem to Compiler Verification

  • 강연자: 허충길 교수 (서울대학교 컴퓨터공학부)

  • 시간 및 장소: 2015년 6월 5일(금요일), 17 ~ 18시 / 연세대학교 과학관 225호
  • 초록: 여기

2014년 2학기

컴퓨터과학자가 파악한 튜링의 원조논문 (Readings of Turing's 1936 Paper)

  • 강연자: 이광근 교수 (서울대학교 컴퓨터공학과)

  • 시간 및 장소: 2015년 7월 21일, 화요일, 16 ~ 17시 / 연세대 과학관 225호

Curry-Howard Isomorphism

  • 이계식 교수 / 매주 금요일 14 ~ 16시 / 연세대학교 과학관 221호

  • 교재: M. Sørensen and P. Urzyczyn, "Lectures on the Curry-Howard Isomorphism"

  • 내용: 주제는 Curry-Howard isomorphism이지만 유형론과 증명론 전반에 대한 소개를 다룹니다.
    • Type-free Lambda calculus, Intuitionistic logic, Simply typed Lambda calculus, Curry-Howard Isomorphism, Classical logic and control operator, First-order logic/arithmetic, Second-order logic/arithmetic and polymorphism, Dependent types

2013년 2학기

Type-amalgamation properties and polygroupoids in stable theories

  • 강연자: 김병한 교수 (연세대학교 수학과)

  • 시간 및 장소: 2013년 10월 11일, 금요일, 16 ~ 17시 / 경북대학교 자연과학대학 102호
  • 초록: We define a family of complete totally categorical first-order theories indexed by n ≥ 2 such that the nth theory has k-uniqueness property for all k ≤ n but fails to have (n+1)-uniqueness. The theories axiomatize structures that are relatives of polyadic groups. We show that such structures must be interpretable in any first-order theory that has k-uniqueness for all k ≤ n but fails (n + 1)-uniqueness. As an application, we give a more precise classification of totally categorical theories of disintegrated type. This is a joint work with John Goodrick and Alexei Kolesnikov.

2013년 1학기

Elementary Patterns of Resemblance

  • 강연자: Gunnar Wilken 박사 (Oist Institute of Science and Technology)
  • 시간 및 장소: 2013년 6월 28일, 금요일, 16:00~17:00 / 연세대학교 과학관 225호
  • 초록: In the first half of my talk, I will talk about the history of proof theory. Then Tim Carlson's access pattern will be introduced. At the end I try to give an overview of describing ordinals with patterns.

모델론에서의 호몰로지군론과 1-껍질을 갖는 2-사슬들의 분류

  • 강연자: 이정욱 (연세대학교 수학과 박사과정)
  • 시간 및 장소: 2013년 4월 19일, 금요일 18:00~19:00 / 연세대학교 과학관 225호

역수학과 증명보조기 (Reverse mathematics and proof assistants)

  • 강연자: 이계식 교수 (한경대학교 웹정보공학과)
  • 시간 및 장소: 2013년 3월 13일, 수요일 17:00~18:00 / 연세대학교 과학관 221호

2012년 2학기

An Example of Logic in Computer Science : Certified Programming with Dependent Types (Part 2)

  • 강연자: 차리서 (고려대학교 컴퓨터·전파통신공학과 박사과정)
  • 시간 및 장소: 2012년 12월 7일, 금요일 16:00~17:00 / 연세대학교 과학관 325호

An Example of Logic in Computer Science : Certified Programming with Dependent Types

  • 강연자: 차리서 (고려대학교 컴퓨터·전파통신공학과 박사과정)
  • 시간 및 장소: 2012년 11월 16일, 금요일 오후 16:00~17:00 / 연세대학교 과학관 227호

2012년 1학기

증명과 계산

  • 강연자: 정주희 교수 (경북대학교 수학교육과)
  • 시간 및 장소: 2012년 2월 10일, 금요일 오후 16:00~17:00 / 연세대학교 과학관 227호

2010년 2학기

수학혁명과 논리

  • 강연자: 박창균 교수 (서경대학교 철학과)
  • 시간 및 장소: 2012년 11월 26일, 금요일 16:00-17:00 / 연세대학교 과학관 225호

2009년 2학기

Forcing, and the Independence of the Continuum Hypothesis: A talk in memory of Cohen

  • 강연자: 김병한 교수 (연세대학교 수학과)
  • 시간 및 장소: 2009년 11월 24일, 화요일 16:00-17:00 / 연세대학교 과학관 225호

Formal proof - Theory and practice

  • 강연자: 기계식 박사 (ROSAEC Center, Seoul National University)
  • 시간 및 장소: 2009년 9월 28일, 월요일 15:00-16:00 / 연세대학교 과학관 225호
  • 초록: A language is a set of symbols each of which has a kind of fixed rule for its use. These rules form the grammar of the language. Following the grammar, one builds formulas and proof systems. A formal language is a language for which there is a purely mechanical process for proofs or verification of a mathematical property. And a formal proof is a proof written in a formal language which can be easily checked by its mechanical process.

In this talk an overview of the current state in formal proof will be given. The main contents are based on the four papers of the Notices of the American Mathematical Society published in November 2008.(http://www.ams.org/notices/200811/index.html)

Decidability and Elimination of Quantifiers

  • 강연자: 정주희 교수 (경북대학교 수학교육과)
  • 시간 및 장소: 2009년 9월 25일, 목요일 11:00~12:00 / 연세대학교 과학관 225호

2009년 1학기

Fast growing functions and logic

  • 강연자: 정주희 교수 (경북대학교 수학교육과)
  • 시간 및 장소: 2009년 3월 23일, 금요일 14:00~15:00 / 연세대학교 과학관 225호

2008년 2학기

Leibniz's Logic

  • 강연자: 박창균 교수 (서경대학교 철학과)
  • 시간 및 장소: 2008년 11월 20일, 목요일 11:00~12:00 / 충북대학교 자연과학대학 수학과 대학원 강의실 (40동 412호실)

귀납적 정의의 집합론적 근거 (Set-theoretic basis of Inductive definitions)

  • 강연자: 이계식 박사 (National Institute of Advanced Industrial Science and Technology (AIST)
  • 시간 및 장소: 2008년 6월 13일, 금요일 11:00~12:00 / 연세대학교 과학관 B130호
  • 초록: 수학 및 논리학에서 일상적으로 사용되는 귀납적 정의는 정의 되는 집합을 구성하는 원소를 생성하는 규칙의 집합으로 표시되며 정의 되는 집합의 어떤 원소도 주어진 규칙에 의거하여 생성된다고 규정한다. 자연수의 집합이 대표적인 예이며 모든 형식언어(formal languages)에서 기본적으로 사용된다. 이번 강연에서는 귀납적 정의의 집합론적 근거와 활용을 살펴본다. Inductive definitions, which are routinely used in mathematics and logic, can be described as a collection of rules that generate the elements of the sets to be defined. And inductive definitions declare that every element of the set be generated only via these rules. Inductive definitions are routinely used in every formal language. The set of natural numbers is a good example. In this lecture, we discuss the set-theoretic basis and applications of inductive definitions.

2007년 2학기

Topology and Computation

  • 강연자: 정주희 교수 (경북대학교 수학교육과)
  • 시간 및 장소: 2007년 12월 18일, 화요일 11:00~12:00 / 연세대학교 과학관 B102호

Ultraproduct and Compactness

  • 강연자: 김선영 (연세대학교 수학과 박사과정)
  • 시간 및 장소: 2007년 12월 7일, 금요일 15:30~17:00 / 연세대학교 과학관 246호

Introduction to the Model Theory of Modules: Positive-primitive formulae

  • 강연자: Ivo Herzog 교수 (연세대학교 수학과)
  • 시간 및 장소: 2007년 9월 21일 ~ 11월 30일, 매주 금요일 15:30~17:00 / 연세대학교 과학관 246호
  • 내용: The first lecture will be devoted to the formal calculus of positive-primitive (pp-) formulae, and the early results in the theory. This will include Baur's elimination of quantifiers up to pp-formulae and the axiomatization of complete theories in terms of invariants statements. Examples from abelian groups will be described.

증명론과 컴퓨터수학 (Proof theory and computer mathematics)

  • 강연자: 이계식 박사 ((ROSAEC Center, Seoul National University)
  • 시간 및 장소: 2007년 9월 14일, 금요일 13:00~14:00 / 연세대학교 과학관 B130호