Daniel's blog

Coq는 주로 소프트웨어와 수학적 증명의 형식적 검증에 사용되는 증명 도우미이다. 수학적 주장, 정의, 정리를 표현하기 위한 공식 언어와 이러한 주장에 대한 증명을 대화식으로 구성하고 검증하는 메커니즘을 제공한다. 전반적으로 Coq는 공식적인 추론과 검증을 위한 강력한 플랫폼을 제공하므로 소프트웨어 개발, 암호화, 안전이 중요한 시스템 등 정확성과 신뢰성이 중요한 영역에서 유용하게 사용할 수 있다. Coq의 주요 기능은 다음과 같다. 종속 유형 (Dependent Types): Coq는 귀납적 구조(Inductive Constructions)의 계산법이라는 유형 이론을 기반으로 한다(따라소 "COQ"라는 이름이 붙었다.). 유형이 용어에 종속되거나 그 반대의 경우도 허용하는 종속 유형을 지원한다. 이 기..

Federated Learning은 로컬 데이터 샘플을 보유한 여러 분산형 edge device 또는 server에서 모델을 교환하지 않고도 학습할 수 있는 머신 러닝 접근 방식이다. 중앙 서버와 같은 한 곳에서 모든 데이터를 수집하는 대신 데이터가 저장된 곳으로 모델을 보내 로컬에서 학습한 다음 학습한 내용(예: model updates 또는 gradients)만 중앙 서버나 aggregator로 다시 보낸다. 이 프로세스는 원시 데이터가 디바이스를 벗어나지 않고 집계된 insight만 공유되므로 사용자 개인정보를 보호하는 데 도움이 된다. 특히 의료(환자 데이터), 금용(거래 기록) 또는 IoT(사물 인터넷) 디바이스와 같이 데이터 개인 정보 보호가 중요한 시나리오에서 유용하다. 또한 네트워크를 통해..

Factory Method Pattern은 객체 지향 프로그래밍에서 사용되는 창조적인 디자인 패턴이다. 이 패턴은 객체의 인스턴스화 프로세스를 서브 클래스에 위임하는 방법을 제공해 애플리케이션 아키텍처의 유연성을 높이고 분리할 수 있도록 한다. 이 패턴은 런타임까지 객체의 정확한 유형과 종속성을 확인할 수 없을 때 유용하다. 주요 개념Creator Classes: 객체를 생성하는 메서드를 선언하는 추상 클래스다. Factory Method 라고도 하는 이 메소드는 제품 클래스의 객체(product class)의 객체를 반환하기 위한 것이다.Concrete Creators: creator class를 상속하고 Factory Method를 재정의해 특정 product의 인스턴스를 반환하는 클래스다.Produ..

Socket Programming은 일반적으로 서로 다른 시스템에서 실행되지만 같은 시스템에 있을 수도 있는 서로 다른 프로세스 간의 통신을 가능하게 하는 방법이다. 본질적으로는 통신 채널의 엔드포인트인 'Socket'을 만드는 것이다. Socket Programming은 네트워크를 통해 통신하는 모든 애플리케이션의 기본이므로 네트워크 소프트웨어 개발에 매우 중요하다. Socket의 정의: Socket은 네트워크에서 실행 중인 두 프로그램 간의 양방향 통신 링크의 endpoint다. Socket읜 포트 번호에 바인딩 되어 TCP 계층에서 데이터가 전송될 애플리케이션을 식별할 수 있다.작동 방식: Socket Programming은 일반적으로 TCP/IP 프로토콜 스택을 사용한다. 데이터는 네트워크 프로토..